theorem leorlt (a b: nat): $ a <= b \/ b < a $;
b < a \/ a <= b -> a <= b \/ b < a
b < a \/ a <= b
a <= b \/ b < a