theorem ltnle (a b: nat): $ a < b <-> ~b <= a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltlenle | a < b <-> a <= b /\ ~b <= a |
|
2 | anr | a <= b /\ ~b <= a -> ~b <= a |
|
3 | 1, 2 | sylbi | a < b -> ~b <= a |
4 | leorlt | b <= a \/ a < b |
|
5 | 4 | conv or | ~b <= a -> a < b |
6 | 3, 5 | ibii | a < b <-> ~b <= a |