proposition: Lemma opow_Mspec x y: \2o <=o x -> ordinalp y -> y <=o (x ^o y).
proof: Proof. move=> x2 y1. move: ord_pow_axioms => [ [ax1 _ _ _] _ _ _]. move: (ord_induction_p9 (erefl opow') ax1 x2 y1); rewrite opow2x //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)