proposition: Lemma opow_Meqltr a b c: \2o <=o a -> ordinalp b -> ordinalp c -> ((b <o c) <-> ( (a ^o b) <o (a ^o c))).
proof: Proof. move=> h ob oc. split; first by apply: opow_Meqlt. move=> aux; case: (oleT_ell oc ob). - by move=> cb; move: aux => [_]; rewrite cb. - by move=> h1;move: (opow_Meqlt h h1) => [/(oltNge aux) ]. - done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)