theorem eqlele (a b: nat): $ a = b <-> a <= b /\ b <= a $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqle | a = b -> a <= b |
|
| 2 | eqler | a = b -> b <= a |
|
| 3 | 1, 2 | iand | a = b -> a <= b /\ b <= a |
| 4 | leasym | a <= b -> b <= a -> a = b |
|
| 5 | 4 | imp | a <= b /\ b <= a -> a = b |
| 6 | 3, 5 | ibii | a = b <-> a <= b /\ b <= a |