theorem leasym (a b: nat): $ a <= b -> b <= a -> a = b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 |
a <= b /\ b <= a -> a <= b |
||
2 |
a <= b /\ b <= a -> b <= a |
||
3 |
a <= b /\ b <= a -> a = b |
||
4 |
a <= b -> b <= a -> a = b |