theorem leorle (a b: nat): $ a <= b \/ b <= a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltle | b < a -> b <= a |
|
2 | leorlt | a <= b \/ b < a |
|
3 | 2 | conv or | ~a <= b -> b < a |
4 | 1, 3 | syl | ~a <= b -> b <= a |
5 | 4 | conv or | a <= b \/ b <= a |