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