proposition: Lemma cpow_Mleeq x y z: x <=c y -> x <> \0c -> x ^c z <=c y ^c z.
proof: Proof. move=> xy xz. by rewrite - cprod_of_same - cprod_of_same; apply: cprod_increasing0 => _ _. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)