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