proposition: Lemma cpow_Meqlt a b b': natp a -> natp b' -> b <c b' -> \1c <c a -> (a ^c b) <c (a ^c b').
proof: Proof. move=> aN b'N bb' l1a. have anz := card_gt_ne0 l1a. have bN:= NS_lt_nat bb' b'N. have [c [cN cnz <-]]:= (card_ltP1 b'N bb'). have le1 := (clt_leT l1a (cpow_Mle1 (CS_nat aN) cnz)). rewrite cpow_sum2; apply: cprod_M1lt;fprops; apply: (cpow_nz anz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)