proposition: Lemma ord_ext_div_exists a b: \2o <=o a -> \0o <o b -> exists x y z, ord_ext_div_pr a b x y z.
proof: Proof. move=> a2 b1. move: (proj32 a2) (proj32_1 b1) => oa ob. case: (oleT_el oa ob); last first. move=> ba; exists \0o; exists b; exists \0o; hnf. rewrite (opowx0 a) (oprod1l ob)(osum0r ob). move: OS0 => o0; split => //; split => //;by apply olt_01. move=> ab. have b11: \1o <=o b by apply/oge1P. move: ord_pow_axioms => [[ax1 _ _ _ ] _ _ _]. move: (ord_induction_p12 (erefl opow') ax1 a2 b11) => [y]. rewrite -(opow2x y a2) -(opow2x (osucc y) a2). move=> [yb fyb fysb]. have oy:=proj31 yb. move: fysb; rewrite (opow_succ oa oy). move:(OS_pow oa oy)=> oay ltb. move: (odivision_exists oay oa ltb)=> [[oq or abq lt1] lt2]. exists y, (oquo b (a ^o y)), (orem b (a ^o y)); split => //; split => //. apply/ord_ne0_pos => // qz; move: abq; rewrite qz (oprod0r) (osum0l or) => h. by apply/(oltNge lt1); rewrite -h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)