proposition: Lemma cpow2_MeqltP n m: natp n -> natp m -> (\2c ^c n <c \2c ^c m <-> n <c m).
proof: Proof. move => sa sb; split => h; last apply: (cpow_Meqlt NS2 sb h clt_12). by case: (NleT_el sb sa) => // /cpow_M2le /(cltNge h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)