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