proposition: Lemma ord_factor9 p n: ofact_list_succ p (csucc n) -> natp n -> ~ (natp (p \0c)) -> exists ec m, [/\ natp m, CNFp_ax1 ec (csucc m), oprodf p (csucc n) = CNFpv1 ec (csucc m), let p' := p \o csucc in Q(ec \0c) = oprodf p' (first_non_int p' n)& P(ec \0c) = odegree (p \0c)].
proof: Proof. move => ha nN; move: ha. move:(cleR (CS_nat nN)). move: n nN {-2} n p. apply: Nat_induction. move => n p /cle0 en0 ha h. set ec0 := (fun i:Set => J (odegree (p \0c)) \1c). rewrite en0 in ha; move:(cltS NS0) => lt01. case: (ord_factor8 ha lt01); first by move => [p0n]; case:h. move: PN1 => pn1 [hb hc hd]. have he: \0o <o odegree (p \0c). case:(ozero_dichot(OS_degree hb)) => // d0. case: hc; rewrite hd d0 oopow0 osucc_one; apply: NS2. have ax1: CNFp_ax1 ec0 (csucc \0c). rewrite /ec0;move => i _ /=; split; aw;fprops. exists ec0, \0c. rewrite en0;split => //. - exact: NS0. - rewrite succ_zero (oprod_f1 hb) (CNFp_1 ax1 lt01) /ec0 /cantor_pmon;aw. by rewrite (CNFp_pr1 he PN1) /CNFp_value2 -hd (oprod1r hb). - rewrite /ec0;move:(first_non_int_p1 (fun i : Set => p (csucc i)) NS0); aw. set k := first_non_int _ _; move => [hh _]; case: hh. by move ->; rewrite oprod_f0. by move => [/clt0]. - by rewrite /ec0 pr1_pair. move => M MN Hrec n p. case /cle_eqVlt; last by move/(cltSleP MN); apply: Hrec. move => nv ofl nn0. pose p' := fun i => p (csucc i). have nN: natp n by rewrite nv; apply:(NS_succ MN). have np :=(succ_positive n). case: (ord_factor8 ofl np); first by move => [p0n]; case:nn0. move => [op0 _ p0v]. have dp0: \0o <o odegree (p \0c). case:(ozero_dichot(OS_degree op0)) => // d0. case: nn0; rewrite p0v d0 oopow0 osucc_one; apply: NS2. move:(first_non_int_p1 p' nN); set k := first_non_int _ _; move =>[kp1 kp2]. set c0:= oprodf p' k. set p'' := fun i => p (i +c csucc k). have obn: ord_below p (csucc n) by move => i /(proj32 (proj1 ofl)); case. have ha: \1c +c n = csucc n by rewrite (Nsucc_rw nN) csumC. have eq1: oprodf p (csucc n) = p \0c *o oprodf p' n by apply:(oprod_f1r). have obn': ord_below p' n by move => i lin; apply:obn; apply/cltSS. have lekn: k <=c n. by case: kp1;[ move ->; apply:(cleR (CS_nat nN))| case; case]. have kN := NS_le_nat lekn nN. have op1: ordinalp c0. apply:(OS_oprodf kN) => i leik; exact:(obn' _(clt_leT leik lekn)). have knN:=(NS_diff k nN). have kdnv:=(cdiff_pr lekn). have eq2: oprodf p' n = c0 *o oprodf p'' (n -c k). rewrite - kdnv in obn'. rewrite - {1}kdnv (oprod_fA (f := p') kN knN obn'); apply: f_equal. by apply: (oprodf_exten knN) => i lin; rewrite /p'' /p' (csum_nS _ kN). have eq3: oprodf p (csucc n) = (p \0c *o c0) *o oprodf p'' (n -c k). have op2:ordinalp (oprodf p'' (n -c k)). apply:(OS_oprodf knN) => i lin; apply: obn. rewrite (csum_nS _ kN); apply:cltSS. by move:(csum_Meqlt kN lin); rewrite kdnv csumC. rewrite eq1 eq2 (oprodA op0 op1 op2); reflexivity. have c0N: posnatp c0. apply:(ord_factor9_aux kN kp2) => j ljk. rewrite /p';exact: ((proj2 ofl) _ (cltSS (clt_leT ljk lekn))). case: kp1 => kp1. set ecl := (fun i:Set => J (odegree (p \0c)) c0). have ax1: CNFp_ax1 ecl (csucc \0c). rewrite/ecl;move => i _ /=; split; aww. exists ecl, \0c; rewrite/ecl; aw. split => //. - exact: NS0. - rewrite eq3 kp1 cdiff_nn oprod_f0 (oprod1r (OS_prod2 op0 op1)). rewrite succ_zero (CNFp_1 ax1 (succ_positive \0c)) /ecl /cantor_pmon; aw. rewrite (CNFp_pr1 dp0 c0N) /CNFp_value2 - p0v. reflexivity. case: (equal_or_not (n -c k) \0c) => lnk. by move:(proj2 (proj1 kp1)); rewrite - kdnv lnk (csum0r (CS_nat kN)). move: (cpred_pr knN lnk); set m := cpred _; move=> [mN nkv1]. have h1: m <=c M. apply/(cleSSP (CS_nat mN) (CS_nat MN)). rewrite - nkv1 - nv. by apply:(cdiff_ab_le_a _ (CS_nat nN)). have h00 i: i <c n -c k -> i +c k <c n. by move => link; move: (csum_Meqlt kN link); rewrite kdnv csumC. have h0 i: i <c csucc m -> (i +c csucc k) <c csucc n. by rewrite - nkv1 => /h00 ln; rewrite (csum_nS _ kN); apply:cltSS. have h2: ofact_list_succ p'' (csucc m). move: ofl => [[s ax1 ax2] ax3]. split; first split. - exact (NS_succ mN). - by move => i /h0 lim; apply: ax1. - move => i iN /h0 lim; rewrite /p''(csum_Sn _ iN); apply: ax2. exact: (NS_sum iN (NS_succ kN)). by rewrite - (csum_Sn _ iN). - by move => i /h0 lim; apply: ax3. have h3:~ natp (p'' \0c). by move: (proj2 kp1); rewrite/p' /p'' (csum0l (CS_succ _)). move:(Hrec m p'' h1 h2 h3) => [ecs [ln1 [r1 r2 r3 r4 r5]]]. set ecf := fun i => Yo (i = \0c) (J (odegree (p \0c)) c0) (ecs (cpred i)). have r1': natp (csucc ln1) by apply: NS_succ. have h01 i: i <c csucc (csucc ln1) -> i <> \0c -> cpred i <c csucc ln1. move => lin inz; move: (NS_lt_nat lin (NS_succ r1')) => iN. move: (cpred_pr iN inz) => [ua ub]. by apply/(cltSSP (CS_nat ua) (CS_succ ln1)); rewrite - ub. have r2':CNFp_ax1 ecf (csucc (csucc ln1)). rewrite/ecf;move => i min. case: (equal_or_not i \0c) => ei0; Ytac0; first split;aww. have r3': oprodf p (csucc n) = CNFpv1 ecf (csucc (csucc ln1)). rewrite eq3 nkv1 r3 {2}/CNFpv1 (oprod_f1r (OS_CNFp0 r2') r1'). apply: f_equal2. rewrite /cantor_pmon/ecf;Ytac0; aw. rewrite (CNFp_pr1 dp0 c0N). rewrite /CNFp_value2 - p0v; reflexivity. apply:(oprodf_exten r1') => i lin. rewrite /ecf /cantor_pmon (cpred_pr2 (NS_lt_nat lin r1')). by rewrite (Y_false (@succ_nz i)). have r4': let p'0 := fun i : Set => p (csucc i) in Q (ecf \0c) = oprodf p'0 (first_non_int p'0 n). rewrite/ecf; Ytac0; rewrite pr2_pair; reflexivity. have r5':(P (ecf \0c)) = odegree (p \0c). by rewrite /ecf Y_true; aw. exists ecf, (csucc ln1); split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)