theorem ltconsid1 (a b: nat): $ a < a : b $;
a <= a, b <-> a < suc (a, b)
a <= a, b <-> a < a : b
a <= a, b
a < a : b