proposition: Lemma opow_Meqle1 x y: \0o <o x -> \0o <o y -> x <=o (x ^o y).
proof: Proof. move=> /oge1P x2 y1. case: (equal_or_not \1o x) => o1. rewrite - o1 opow1x; apply: oleR; fprops. have o3: \2c <=o x by apply /oge2P; split. move: ord_pow_axioms => [ [ax1 _ _ _] _ _ _]. move: (ord_induction_p4 (erefl opow') ax1 o3 y1);rewrite opow2x //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)