theorem lenlt (a b: nat): $ a <= b <-> ~b < a $;
(b < a <-> ~a <= b) -> (a <= b <-> ~b < a)
b < a <-> ~a <= b
a <= b <-> ~b < a