proposition: Lemma cpow_Mle1 a b: cardinalp a -> b <> \0c -> a <=c (a ^c b).
proof: Proof. move=> ca l1b. case: (equal_or_not a \0c); first by move => ->; apply: cle0x; fprops. move=> anz;rewrite - cpowcr - {1} (cpowx1 ca); apply:(cpow_Meqle anz). by apply:(cge1 (CS_cardinal b)); apply: card_nonempty0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)