theorem lebool (a b: nat): $ a <= b -> bool b -> bool a $;
a <= b -> b < 2 -> a < 2
a <= b -> bool b -> bool a