proposition: Lemma critical_product_P2: let CP := critical_ordinal \1o oprod2 in let p1 := fun y => [/\ infinite_o y, ordinalp y & (forall z, \1o <o z -> z <=o y -> exists2 t, ordinalp t & y = z ^o t)] in forall y, CP y <-> p1 y.
proof: Proof. move=> CP p1 y. have Hc: infinite_o y /\ ordinalp y <-> omega0 <=o y. split. move =>[qa qb];move/ (omega_P1 qb): qa=> sop; split => //; apply:OS_omega. by move => [_ qa qb]; split => //; move/(omega_P1 qa): qb. move: (critical_productP y) => [Ha Hb]. split. move/Hb/Ha => [oy etc]; move/Hc: (oy) => [qa qb]; split => //. by move=> z z1 z2; move: (etc _ z1 z2) => [t [t1 t2 t3]]; exists t. move=> [ify oy hy]; move/Hc: (conj ify oy) => loy. have lt1y:= (olt_leT olt_1omega loy). split => // x le1x ltxy; move:(ltxy) => [lexy nexy]. have ox:= proj31 lexy. move:(olt_leT olt_01 le1x) => xp. case: (oone_dichot xp) => xl1; first by rewrite xl1 (oprod1l oy). move: (hy _ xl1 lexy) => [t ot yt]. case: (rev_succ_pr ot); last first. by rewrite {1} yt - {1} (opowx1 ox) - (opow_sum ox OS1 ot) => <-. have yn1:= nesym (proj2 lt1y). have xl2: \2o <=o x by apply oge2P. move => tf; move: yt. case: (ozero_dichot ot); first by move => ->; rewrite opowx0. move=> tnz yt. apply: oleA; last by apply: oprod_M1le. move: OS0 OS1 OS2 olt_02=> os0 os1 os2 l02. case: (equal_or_not t \2o) => tnt. move: (opow_Mspec2 OS2 xl2). rewrite - {2} tnt -yt => leby. have xx: y = x *o x. rewrite yt tnt - osum_11_2 opow_sum // opowx1 //. have lexx2: x <=o (x *o \2o) by apply: oprod_Mle1. have b1:= olt_leT xl1 lexx2. move: (hy _ b1 leby) => [u ou yuv]. case: (ord2_trichotomy ou) => uz; first by move: yuv; rewrite uz opowx0. move: yuv; rewrite uz (opowx1 (proj32 lexx2)) => eq1. rewrite {1} eq1 oprodA // xx -{1} xx eq1 - oprodA //. apply: oprod_Mlele; fprops. case: (oleT_el OS_omega ox) => oxo. have l2o: \2o <o omega0 by apply:olt_2omega. exact: (oleT(proj1 (oprod2_lt_omega l2o l2o)) oxo). by move: (oprod2_lt_omega oxo oxo); rewrite - xx => /(oleNgt loy). move: (odiff_pr uz) =>[]; set v := u -o \2o => v1 v2. move: yuv; rewrite v2 opow_sum //; last by fprops. set w := ((x *o \2o) ^o \2o) => le1. have od: ordinalp (x *o \2o) by fprops. have : y = w. apply: oleA. rewrite /w yt tnt; apply: (opow_Mleeq (nesym (proj2 xp)) lexx2 OS2). rewrite le1; apply: oprod_Mle1; rewrite /w; fprops. apply:(opow_pos) => //; apply: oprod2_pos => //. rewrite /w yt tnt; move => /(ord_square_inj ox) => h. by move: (proj2 xp); rewrite h; case. rewrite {1} yt - {1} (opowx1 ox) - opow_sum //. have tb: natp t by apply /olt_omegaP. have tnz':= nesym (proj2 tnz). move: (cpred_pr tb tnz') => []; set u := (cpred t) => [uB tsu]. have uo: u <o omega0 by apply /olt_omegaP. have ou:= proj31_1 uo. have us: t = osucc u. by rewrite tsu; apply: succ_of_finite; move: uB => /NatP. set z := x ^o u. case: (equal_or_not u \0o) => unz. case: nexy; rewrite yt tsu unz // succ_zero opowx1 //. have z1: \1o <o z. by rewrite /z - (opowx0 x) - opow_Meqltr //; apply:ord_ne0_pos. have oz:= proj32_1 z1. have z2: z <=o y. rewrite /z yt; apply: opow_Meqle => //. by rewrite us;move: (oltS ou) => [ok _]. move: (hy _ z1 z2) => [v ov]. case: (ord2_trichotomy ov). by move => ->; rewrite opowx0. move => ->; rewrite opowx1 // /z us yt. move=> se; move: (opow_regular xl2 ot ou se); rewrite us => bad. by move: (oltS ou) => [_]; rewrite bad. move=> v2. have le1: (u +o u <=o (u *o v)). rewrite - (ord_double ou); apply: oprod_Meqle => //. suff aux : ((\1o +o osucc u) <=o (u +o u)). move => yv; rewrite yv /z - opow_prod //. apply: opow_Meqle => //; rewrite us; exact: (oleT aux le1). have ->: \1o +o osucc u = u +o \2o. have oB := NS1. have tB:= NS2. have su: natp (osucc u) by ue. have fcu: finite_c u by apply /NatP. rewrite osum2_2int // osum2_2int // - succ_of_finite // (Nsucc_rw uB). by rewrite csumC - csumA csum_11. apply: osum_Meqle => //. case: (ord2_trichotomy ou);[ done | move => u1 | done ]. by case: tnt; rewrite us u1 osucc_one. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)