proposition: Lemma cpow_M1lt a b: cardinalp a -> \1c <c b -> a <c (b ^c a).
proof: Proof. move => ca /(cleSltP NS1); rewrite succ_one => h. apply: (clt_leT (cantor ca)); apply:(cpow_Mleeq _ h card2_nz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)