proposition: Lemma oprod_fix2 a x: \0o <o a -> ordinalp x -> a *o x = x -> exists2 y, ordinalp y & x = a ^o omega0 *o y.
proof: Proof. move => ap ox xp. case: (oquoremP ox (opow_pos ap OS_omega)). set q:= (oquo _ _); set r := orem _ _;move=> oq or xv rs. have oa:= proj32_1 ap. have ofp:=(OS_prod2 (proj32_1 rs) oq). move: (oprodD ofp or oa); rewrite -xv xp xv (oprod_fix1 ap oq) => eq1. move:( osum2_simpl or (OS_prod2 oa or) ofp eq1) => rar. have ran: forall n, inc n Nat -> r = a ^o n *o r. apply: Nat_induction; first by rewrite opowx0 oprod1l. move => n nN h; move:(OS_nat nN) => os. have ->: csucc n = \1o +o n. by rewrite (osum2_2int NS1 nN) csumC Nsucc_rw. by rewrite (opow_sum oa OS1 os)(opowx1 oa) -(oprodA oa (OS_pow oa os) or) -h. case:(equal_or_not r \0o) => rz; first by exists q => //; rewrite rz osum0r. case: (oone_dichot ap) => a2. by move: rs rz; rewrite a2 opow1x; move /olt1. case:(oltNge rs). move/oge2P : a2 => a2; rewrite(proj2 (opow_normal a2) _ omega_limit). apply: ord_ub_sup => //. move => w /funI_P [n nN ->]. rewrite (ran _ nN); move:(OS_nat nN) => os. by apply:oprod_Mle1; [ fprops | apply/ord_ne0_pos ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)