theorem lttr (a b c: nat): $ a < b -> b < c -> a < c $;
a <= b -> b < c -> a < c
a < b -> a <= b
a < b -> b < c -> a < c