proposition: Lemma cpow_Meqle x a b: x <> \0c -> a <=c b -> x ^c a <=c x ^c b.
proof: Proof. move => /card_nonempty0 xnz /proj33 leab. rewrite - cpowcl -(cpowcl x b) - 2! cprod_of_same /cprodb. rewrite - (restr_Lg (fun _ => (cardinal x)) leab). apply: cprod_increasing1;hnf; aw; trivial => z zx; rewrite LgV //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)