pub theorem axext (a b: nat): $ a == b -> a = b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssle | a C_ b -> a <= b |
|
| 2 | eqss | a == b -> a C_ b |
|
| 3 | 1, 2 | syl | a == b -> a <= b |
| 4 | ssle | b C_ a -> b <= a |
|
| 5 | eqssr | a == b -> b C_ a |
|
| 6 | 4, 5 | syl | a == b -> b <= a |
| 7 | 3, 6 | leasymd | a == b -> a = b |