theorem necom (a b: nat): $ a != b -> b != a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con3 | (b = a -> a = b) -> ~a = b -> ~b = a |
|
2 | 1 | conv ne | (b = a -> a = b) -> a != b -> b != a |
3 | eqcom | b = a -> a = b |
|
4 | 2, 3 | ax_mp | a != b -> b != a |