proposition: Lemma cpow_Mltle a a' b: natp a' -> natp b -> a <c a' -> b <> \0c -> (a ^c b) <c (a' ^c b).
proof: Proof. move=> a'N bN aa' nzb. move:b bN nzb; apply:Nat_induction => // n nN hrec _. case: (equal_or_not n \0c) => nz. by rewrite nz succ_zero (cpowx1 (proj31_1 aa')) (cpowx1 (proj32_1 aa')). rewrite (cpow_succ _ nN) (cpow_succ _ nN). apply:(cprod_Mlelt (NS_pow a'N nN) a'N (proj1 (hrec nz)) aa'). exact: (cpow_nz (card_gt_ne0 aa') (b:=n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)