proposition: Lemma opow_normal x: \2o <=o x -> normal_ofs (opow x).
proof: Proof. move=> x2; move: ord_pow_axioms => [[ax1 ax2 _ _ ] _ _ _]. move: (ord_induction_p10 (erefl opow') ax1 x2). have op: forall y, x ^o y = opow' x y by move=> y ; apply: opow2x. move => [pa pb];split; first by move => u v; rewrite /= op op; apply: pa. by move => a al; rewrite op (pb _ al); apply: ord_sup_2funI => u; rewrite op. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)