theorem ltnlt (a b: nat): $ a < b -> ~b < a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltnle | a < b <-> ~b <= a |
|
2 | con3 | (b < a -> b <= a) -> ~b <= a -> ~b < a |
|
3 | ltle | b < a -> b <= a |
|
4 | 2, 3 | ax_mp | ~b <= a -> ~b < a |
5 | 1, 4 | sylbi | a < b -> ~b < a |