proposition: Lemma cpow_Mlele a b a' b': a <> \0c -> a <=c a' -> b <=c b' -> (a ^c b) <=c (a' ^c b').
proof: Proof. move=> nz aa' bb'; apply: (cleT (cpow_Mleeq b aa' nz)). by apply:cpow_Meqle bb'; dneg az; apply:cle0; rewrite -az. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)