proposition: Lemma ord_factor_exits x: \0o <o x -> exists p n, [/\ ord_factor_list p n, natp n & x = oprodf p n].
proof: Proof. move => xp; move:(CNFp_exists xp) => [p [n [[ax1 ax2] nN ->]]]. have Hu a: posnatp a -> natp a /\ \1c <=c a. by move=> [aN /proj2/nesym ap]; split => //;apply: (cge1 (CS_nat aN)). rewrite /CNFpv. move: (Hu _ (proj33 ax2)); set lc := Q (p n). move => [lcN lcp]; move:(nat_prime_p7 lcN lcp) => [p1 [n1 [axp1 n1N f1v]]]. move: (CNFr_exists (proj32 ax2)) => [f [n2 [n2N axf2 ->]]]. set y := oopow _. pose oo t := oopow (oopow t). have oop t: ordinalp t -> ord_prime (oo t). by move => ot;apply/ord_prime_p1; constructor 3; exists t. pose r i := (oo (f (cpred (n2 -c i)))). have oopm a b: a <=o b -> oo a <=o oo b. move => h; exact (opow_Mo_le (opow_Mo_le h)). have oopsm a b: a <o b -> oo a <o oo b. move => h; exact (opow_Mo_lt (opow_Mo_lt h)). have ooi a b: ordinalp a -> ordinalp b -> oo a = oo b -> a = b. by move => oa ob eq; case: (oleT_ell oa ob) => // /oopsm; rewrite eq; case. have of2: ord_factor_list r n2. split; first exact: n2N. by move => i lin; apply: oop; apply (proj1 axf2); apply:cdiff_lt_symmetry. move => i iN ltsin. move:(cdiff_A1 n2N iN (proj1 ltsin)); set j1 := cpred _ => j1v. move: (NS_diff (csucc i) n2N); rewrite - j1v => j1N. have j1nz: j1 <> \0c. move=> h; move: ltsin => [h']; case; move:(cdiff_pr h'). by rewrite - j1v h csum0r //; apply: CS_succ. have lt1: j1 <c n2. rewrite - (cdiff_pr (proj1 ltsin)) - j1v csumC; apply:(csum_M0lt j1N). apply: succ_nz. move:(cpred_pr j1N j1nz) => [pj1 pj1v]. move: (proj2 axf2 (cpred j1));rewrite - pj1v => h; move:(h pj1 lt1) => lt2. split. move: (oopm _ _ (ole0x (proj32 lt2))). by rewrite /oo oopow0 oopow1 => W /oltNge. move => q op; rewrite /r - j1v -/(oo _) => eq1; exists (f j1) => //. by rewrite -(ooi _ _ (proj31 lt2) op eq1). have Hw i: i <c n2 -> cpred (n2 -c i) <c n2. move => lin2; have iN := (NS_lt_nat lin2 n2N). move/(cleSltP iN): lin2 => sil2n. rewrite (cdiff_A1 n2N iN sil2n); apply:(cdiff_Mlt n2N n2N sil2n). apply: (csum_M0lt n2N (@succ_nz _)). have Hv i : i <c n2 -> limit_ordinal (r i). move => lin2; apply:indecomp_limit2; apply:oopow_pos. apply:(proj1 axf2 _ (Hw i lin2)). have yv: y = oprodf r n2. rewrite (proj33 (@ord_factor4 r n2 of2 Hv)). apply: f_equal; apply:(osumf_exten n2N) => i il2. have ofi := (proj1 axf2 _ il2). have iN := (NS_lt_nat il2 n2N). move/(cleSltP iN): il2 => sil2n. rewrite (cdiff_A1 n2N iN sil2n) /r (double_diff n2N sil2n) (cpred_pr2 iN). by rewrite (odegree_opow (OS_pow OS_omega ofi)) (odegree_opow ofi). suff: (exists p3 n3, [/\ ofact_list_succ p3 n3, natp n3, (\0c <c n3 -> ord_ptypeI (p3 \0c)) & oprodf p3 n3 = CNFpv1 p n ]). move => [p3 [n3 [[axp3 asp3] n3N p30_spec eq3]]]. set n4 := (n2 +c n1) +c n3. pose p4 i := Yo (i <c n2) (r i) (Yo (i <c (n2 +c n1)) (p1 (i -c n2)) (p3 (i -c (n2 +c n1)))). have n21N := (NS_sum n2N n1N). have n4N := (NS_sum n21N n3N). have all_prime: forall i, i <c n4 -> ord_prime (p4 i). move => i lin; rewrite /p4; move:(NS_lt_nat lin n4N) => iN. case: (NleT_el n2N iN) => n2i; last first. Ytac0; exact:(proj32 of2 i n2i). rewrite (Y_false (cleNgt n2i)); case (NleT_el n21N iN) => n21i. rewrite (Y_false (cleNgt n21i)); apply: (proj32 axp3). apply: (csum_lt2r n21N (NS_diff (n2 +c n1) iN) n3N). by rewrite csumC (cdiff_pr n21i) csumC. have lt1: i -c n2 <c n1. apply:(csum_lt2r n2N (NS_diff n2 iN) n1N). by rewrite csumC (cdiff_pr n2i) csumC. Ytac0; exact:(nat_prime_p1 (proj32 axp1 _ lt1)). have ofl4: ord_factor_list p4 n4. split; [exact | exact | move => i iN lin4; rewrite /p4]. case: (NleT_el n2N iN) => n2i; last first. case:(NleT_el n2N (NS_succ iN)) => lt3; last first. Ytac0; Ytac0; exact:(proj33 of2 i iN lt3). move/(cleSltP iN): (n2i) => lt4. move: (cleA lt3 lt4) => sin2. have lt5: ~ (csucc i <c n2) by rewrite - sin2; case. Ytac0; Ytac0; rewrite sin2 cdiff_nn. have ha: cpred (n2 -c i) <c n2 by apply: Hw. move: (oopm _ _ (ole0x (proj1 axf2 _ ha))). rewrite -/(r i) /oo oopow0 oopow1 => /oltNge W. split; [ by move/W | move => q op uv]. move: (indecomp_limit2 (oopow_pos op)); rewrite - uv. set u := Yo _ _ _ => lu. suff su: osuccp u by case: (limit_nonsucc' lu su). rewrite /u - sin2; case: (equal_or_not n1 \0c) => n1z. have nn2: ~(n2 <c n2) by case. have n20:= (csum0r (CS_nat n2N)). move: lin4; rewrite /n4 n1z n20 - sin2; Ytac0. case: (equal_or_not \0c n3) => [n3z | /(strict_pos_P n3N) /asp3 n3p ]. by rewrite -n3z n20. by move => _; rewrite cdiff_nn. rewrite (Y_true (csum_M0lt n2N n1z)). by move/(strict_pos_P1 n1N): n1z => /(proj32 axp1)/ord_ptypeF_prop []. rewrite (Y_false (cleNgt n2i)) (Y_false (cleNgt (cleT n2i (cleS iN)))). case: (NleT_el n21N iN) => n21i; last first. case:(NleT_el n21N (NS_succ iN)) => lt3; last first. have diN := (NS_diff n2 iN). have lt1 :(csucc (i -c n2)) <c n1. apply: (csum_lt2r n2N (NS_succ diN) n1N). by rewrite (csum_Sn _ diN) csumC (cdiff_pr n2i) csumC. Ytac0; Ytac0; rewrite (cdiffSn iN n2i). split; first by move => _ _; apply: (proj33 axp1 _ diN lt1). move /olt_omegaP :(proj31 (proj32 axp1 _ lt1)) => lt4 q op H. move: lt4; rewrite H => /oltNge; case; rewrite -{1}(opowx1 OS_omega). apply/opow_Mo_le; rewrite - (opowx0 omega0);apply/opow_Mo_le. by apply: ole0x. have le4: n2 +c n1 = csucc i by apply:(cleA lt3); apply/(cleSltP iN). have lt5: ~(csucc i <c csucc i) by case. Ytac0; rewrite le4 (Y_false lt5) cdiff_nn. have lt6: i -c n2 <c n1 by apply: (cdiff_Mlt n1N iN n2i); rewrite csumC. move:(proj32 axp1 _ lt6) => np6. have n3p: \0c <c n3. apply /(strict_pos_P1 n3N) => n3z; case: (proj2 lin4). by rewrite /n4 - le4 n3z (csum0r (CS_sum2 n2 n1)). move: (p30_spec n3p) => /ord_ptypeI_prop [wp1 wp2]. split; first by move => _ /oleNgt; case. move => q op pv; case:(limit_nonsucc' _ wp1); rewrite pv. by apply:indecomp_limit2; apply:(oopow_pos op). have lt5 := (cleT n21i (cleS iN)). rewrite (Y_false (cleNgt n21i))(Y_false (cleNgt lt5)). have: csucc i -c (n2 +c n1) <c n3. apply: (csum_lt2r n21N (NS_diff (n2 +c n1) (NS_succ iN)) n3N). by rewrite csumC (cdiff_pr lt5) csumC. rewrite (cdiffSn iN n21i). move => lt4. exact: (proj33 axp3 _ (NS_diff (n2 +c n1) iN) lt4). move:(ord_factor1 ofl4) => obl4. have obl4s: ord_below p4 (n2 +c n1). move => i lin; apply:obl4; apply: (clt_leT lin); apply:csum_M0le; fprops. have ->: (y *o lc) *o CNFpv1 p n = oprodf p4 n4. rewrite (oprod_fA n21N n3N obl4)(oprod_fA n2N n1N obl4s). have <-: y = oprodf p4 n2. by rewrite yv; apply: (oprodf_exten n2N) => i lin; rewrite /p4; Ytac0. set u2 := oprodf _ _; set u3 := oprodf _ _. have ->: CNFpv1 p n = u3. rewrite - eq3; apply:(oprodf_exten n3N) => i lin. have le1: n2 +c n1 <=c i +c (n2 +c n1). apply:csum_Mle0; fprops. move:(cleT (csum_M0le n1 (CS_nat n2N)) le1) => le2. rewrite /p4 (Y_false (cleNgt le1)) (Y_false (cleNgt le2)). by rewrite (cdiff_pr1 (NS_lt_nat lin n3N) n21N). have <- //: lc = u2. rewrite - f1v;apply: (oprodf_exten n1N) => i lin. have le1: i +c n2 <c n2 +c n1 by rewrite csumC;exact: (csum_Meqlt n2N lin). move:(cleNgt (Nsum_M0le i n2N)); rewrite csumC => lt2. by rewrite /p4; Ytac0; Ytac0; rewrite (cdiff_pr1 (NS_lt_nat lin n1N) n2N). by exists p4, n4. have ax2' : forall i, i <c n -> posnatp (Q (p i)). by move => i /ax1/proj33. clear y oo oop r oopm oopsm ooi of2 Hw Hv yv. clear p1 n1 axp1 n1N f1v f n2 axf2 n2N lc lcN lcp ax2. move: n nN ax1 ax2'; apply: Nat_induction. move => _ _; exists (fun i:Set => \1c), \0c; split => //. - split; first by split; [ exact:NS0 | move => i /clt0 | move => i _ /clt0 ]. by move => i /clt0. - apply: NS0. - by case. - by rewrite /CNFpv1 oprod_f0 oprod_f0. move => n nN Hrec ax1 ax2. move:(true_below_rec nN ax1) =>[ax11 [_ ax12 _]]. move:(true_below_rec nN ax2) =>[ax21 ax22]. move: (Hrec ax11 ax21) =>[p1 [n1 [r1 n1N r2 r3]]]. move: (Hu _ ax22)=> [lcN lcp]. move:(nat_prime_p7 lcN lcp) => [p2 [n2 [axp2 n2N f2v]]]. pose f1:= osucc (oopow (P (p n))). pose p3 i := Yo (i <c n1) (p1 i) (Yo (i = n1) f1 (p2 (i -c (csucc n1)))). have sn1N:= (NS_succ n1N). move: (NS_sum sn1N n2N);set n3 := (csucc n1) +c n2; move => n3N. have r5: \0c <c n3 -> ord_ptypeI (p3 \0c). move => r3p; rewrite /p3; case: (equal_or_not n1 \0c) => n1z. have nnO: ~(\0c <c \0c) by case. by rewrite n1z; Ytac0; Ytac0; exists (P (p n)). by move /(strict_pos_P1 n1N) :n1z => n1p; Ytac0; apply: r2. have of2x:= (OS_pow OS_omega (proj32_1 ax12)). have f1p: ord_ptypeI f1 by exists ( P(p n)). have alsp i: i <c n3 -> osuccp (p3 i). move => lin; rewrite /p3. have iN:= NS_lt_nat lin n3N. case: (NleT_el n1N iN) => lt1; last by Ytac0; exact: (proj2 r1 i lt1). rewrite (Y_false (cleNgt lt1)). case: (cle_eqVlt lt1) => lt2. by rewrite lt2 (Y_true (erefl i)) /f1; exists (oopow (P (p n))). rewrite (Y_false (nesym (proj2 lt2))). move/(cleSltP n1N): lt2 => lt3. have lt4: i -c csucc n1 <c n2 by apply:(cdiff_Mlt n2N iN lt3);rewrite csumC. by case: (ord_ptypeF_prop (proj32 axp2 _ lt4)). have opl i: i <c n3 -> ord_prime (p3 i). move => lin; rewrite /p3. have iN:= NS_lt_nat lin n3N. case: (NleT_el n1N iN) => lt1; last first. Ytac0; exact: (proj32 (proj1 r1) i lt1). rewrite (Y_false (cleNgt lt1)). case: (cle_eqVlt lt1) => lt2. rewrite lt2 (Y_true (erefl i)) /f1. by apply:(succ_pow_omega_prime (proj32_1 ax12)). rewrite (Y_false (nesym (proj2 lt2))). move/(cleSltP n1N): lt2 => lt3. have lt4: i -c csucc n1 <c n2. by apply:(cdiff_Mlt n2N iN lt3);rewrite csumC. exact: (nat_prime_p1 (proj32 axp2 _ lt4)). have r4 : ofact_list_succ p3 n3. split; [ split; [ exact | exact | ] | exact]. move => i iN lin3; rewrite /p3. move: (ord_ptypeI_prop f1p) => [f1p1 f1p2]. case: (NleT_el n1N iN) => lin1; last first. move/(cleSltP iN): (lin1) => /cle_eqVlt; case => lt2. have nn: ~(csucc i <c n1) by rewrite lt2; case. Ytac0; Ytac0; Ytac0; split;first by move => _ /oltNge; case. move => q op eqf1. have lf1: limit_ordinal f1. by rewrite eqf1; apply:indecomp_limit2; apply:oopow_pos. case: (limit_nonsucc' lf1 f1p1). Ytac0; Ytac0;exact: (proj33 (proj1 r1) i iN lt2). move: (cle_ltT lin1 (cltS iN)) => [lt2 lt3]. rewrite (Y_false (cleNgt lin1)) (Y_false (cleNgt lt2)); Ytac0. have Hk q j: ordinalp q -> j <c n2 -> p2 j <> oopow (oopow q). move => op /(proj32 axp2)/ord_ptypeF_prop [_ /oltNge js] eq; case: js. move:(opow_Mo_le (opow_Mo_le (ole0x op))). by rewrite oopow0 oopow1 - eq. case: (equal_or_not i n1) => ein1; Ytac0. rewrite ein1 cdiff_nn; split; first by case/oltNge. have lt1: \0c <c n2. apply/(strict_pos_P1 n2N)=> n2z;move:(proj2 lin3). rewrite /n3 n2z ein1 csum0r;fprops. move=> q op eq1; case: (Hk q \0c op lt1 eq1). have lt4: csucc n1 <=c i by apply/(cleSltP n1N); split; [exact | apply:nesym]. have eq4:= (cdiffSn iN lt4); rewrite eq4. have lt5: csucc (i -c csucc n1) <c n2. rewrite - eq4;apply:(csum_lt2r sn1N (NS_diff (csucc n1) (NS_succ iN)) n2N). by rewrite csumC (cdiff_pr (cleSS lin1)) csumC. have dN:= NS_diff (csucc n1) iN. split; first by move => _ _; exact: (proj33 axp2 _ dN lt5). move => q op eq1; case:(Hk q _ op lt5 eq1). have r6: oprodf p3 n3 = CNFpv1 p (csucc n). have obl:= (ord_factor1 (proj1 r4)). have ln1n3: n1 <c n3 by apply:(clt_leT (cltS n1N)); apply:csum_M0le; fprops. have of1: ordinalp (oprodf p1 n1). apply:(OS_oprodf n1N) => i lin; move:(obl i (clt_ltT lin ln1n3)). by rewrite /p3;Ytac0. have of2 :=(OS_succ of2x). have Ha i: i <c n2 -> (p3 (i +c csucc n1)) = (p2 i). move => lin. have lt2: n1 <c i +c (csucc n1). by apply:(clt_leT (cltS n1N)); apply:csum_Mle0; fprops. rewrite /p3 (cdiff_pr1 (NS_lt_nat lin n2N) sn1N). by rewrite (Y_false (cleNgt (proj1 lt2))) (Y_false (nesym (proj2 lt2))). have of3: ordinalp (oprodf p2 n2). apply:(OS_oprodf n2N) => i lin. move:(csum_Mlteq sn1N lin); rewrite (csumC n2) -/n3 => lim. by move:(obl _ lim); rewrite (Ha i lin). rewrite /CNFpv1 (oprod_fS _ nN) {2} /cantor_pmon (CNFp_pr1 ax12 ax22). rewrite /CNFp_value2 - f2v (oprod_fA sn1N n2N obl) -/(CNFpv1 _ _) - r3. rewrite (oprodA of1 of2 of3) (oprod_fS _ n1N); apply: f_equal2. apply: f_equal2. by apply:(oprodf_exten n1N) => i lin; rewrite /p3; Ytac0. have nn: ~ (n1 <c n1) by case. by rewrite /p3; Ytac0; Ytac0. by apply:(oprodf_exten n2N) => i /Ha. by exists p3, n3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)