theorem ltne (a b: nat): $ a < b -> a != b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltirr | ~b < b |
|
| 2 | lteq1 | a = b -> (a < b <-> b < b) |
|
| 3 | 2 | bi1d | a = b -> a < b -> b < b |
| 4 | 3 | com12 | a < b -> a = b -> b < b |
| 5 | 4 | con3d | a < b -> ~b < b -> ~a = b |
| 6 | 5 | conv ne | a < b -> ~b < b -> a != b |
| 7 | 1, 6 | mpi | a < b -> a != b |