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