proposition: Lemma critical_productP (CP := critical_ordinal \1o oprod2) (p1 := fun y => (exists2 n, ordinalp n & y = oopow (oopow n))) (p2 := fun y => omega0 <=o y /\ (forall z, \1o <o z -> z <=o y -> exists t, [/\ ordinalp t, indecomposable t & y = z ^o t])): forall y, (p1 y <-> p2 y) /\ (CP y <-> p1 y).
proof: Proof. move: olt_01 olt_1omega OS_omega OS1=> l01 lt1o oo o1. have auxP: forall y, ordinalp y -> (infinite_o y <-> (omega0 <=o y)). move=> y oy; split; first by move/(omega_P1 oy) => h; split => //. by move => [_ _ ] /(omega_P1 oy). have p21: forall y, p2 y -> p1 y. move=> y [iy yp]. move: (yp _ lt1o iy) => [t [ot oit yv]]. move: (indecomp_prop3 oit) => [n on tb]; exists n => //;ue. have p02: forall y, CP y -> p2 y. move=> y [pa pc pd]; split => //. move=> z z1 lezy; case: (equal_or_not z y) => zy. exists \1o; rewrite zy (opowx1 (proj32 pa)). split => //; apply: indecomp_one. have ltzy: z <o y by split. move: (olt_leT olt_0omega pa) => y1. have z2: \2o <=o z by rewrite - osucc_one ; apply /oleSltP. have oz:= proj32 z2. move: (ord_ext_div_exists z2 y1) => [a [b [c [oa ob oc [bv ltc ltv bnz]]]]]. set x1:= (z ^o a) *o b. have le1: (z ^o a) <=o x1 by rewrite /x1; apply: oprod_Mle1; fprops. have cx1 := olt_leT ltc le1. have co:=ole0x oc. have za1: \1o <=o (z ^o a) by move /oge1P: (ole_ltT co ltc). have le2:= oleT za1 le1. have ox1:= proj32 le1. have oza:= proj32 za1. case: (equal_or_not x1 y) => yx1; last first. have ltx1y: x1 <o y by split => //; rewrite bv; apply: osum_Mle0. move: (pd _ le2 ltx1y). move: (ord_rev_pred y1); set u := (y -o \1o); move => [ou yv]. rewrite {1} yv bv -/x1 (oprodD OS1 ou ox1) (oprod1r ox1). move=> aux1; move: (osum2_simpl (OS_prod2 ox1 ou) oc ox1 aux1) => e1. case: (ozero_dichot ou) => uz. by move: pc; rewrite yv uz (osum0r OS1); case. by move: (oprod_Mle1 ox1 uz); rewrite e1 => /(oltNge cx1) []. case: (equal_or_not (z ^o a) y) => zay; last first. have lt1: (z ^o a) <o y by split=> //; rewrite - yx1. move: (pd _ za1 lt1); rewrite -{2} yx1 /x1 => aux1. have zaz: \0o <o z ^o a by apply/oge1P. case:(oleNgt lezy). by rewrite (oprod2_simpl (proj32 pa) ob zaz aux1). rewrite - zay; exists a;split => //. case: (ozero_dichot oa) => az. by move: pc=> [_ xx]; case: xx;rewrite - zay az opowx0. apply /indecompP => // d da. have od:= proj31_1 da. have znz: \0o <o z by exact: (olt_leT bnz (proj1 ltv)). have ad1: \1o <=o (z ^o d) by apply /oge1P;apply: opow_pos. move: (opow_Meqlt z2 da); rewrite zay => p4. move: (pd _ ad1 p4); rewrite - zay - opow_sum => //. apply: opow_regular => //; fprops. suff p10: forall y, p1 y -> CP y. move=> y; split; split => h. - by apply:p02; apply: p10. - by apply: p21. - by apply: p21; apply: p02. - by apply:p10. move=> y [n on yv]. have yif: omega0 <=o y. rewrite yv - {1} oopow1; apply: opow_Mo_le. apply: (oge1 (OS_pow oo on) (oopow_nz on)). have oy:= (proj32 yif). split; [ exact | exact:(olt_leT lt1o yif) | ]. by rewrite yv => x x1 x2; exact: (oprod_crit_aux on x1 x2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)