theorem leb1tr (a b: nat): $ a <= b $ > $ a <= b1 b $;
a < b1 b -> a <= b1 b
a <= b
a < b1 b
a <= b1 b