proposition: Lemma opow_Mo_leP a b: ordinalp a -> ordinalp b -> (a <=o b <-> (oopow a) <=o (oopow b)).
proof: Proof. move=> oa ob; split; first apply:opow_Mo_le. move => loo. by case: (oleT_el oa ob) => //; move/(opow_Mo_lt) => /oltNge. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)