proposition: Lemma CNFp_p3 e c n: CNFb_axo e c (csucc n) -> natp n -> exists p, [/\ CNFp_ax p n, CNFbvo e c (csucc n) = CNFpv p n, (forall i, i <c n -> (p i) = J (e (csucc i) -o (e i) ) (c (csucc i))) & p n = J (e \0c) (c \0c) ].
proof: Proof. move => ax nN; move: n nN ax; apply: Nat_induction. move => h0; exists (fun z => J (e \0c) (c \0c)). move: (h0) => [[ha hb hc hd] he]. move: (@succ_positive \0c) => qa. move: (hb _ qa) (hc _ qa) (he _ qa) => a1 a2 a4. have qb: posnatp (c \0c) by apply/posnat_ordinalp. have oc:= OS_prod2 (OS_pow OS_omega a1) (proj31_1 a2). split => //. - split; [ by move => i /clt0 | split; aww]. - rewrite /CNFpv CNFp_0 succ_zero /CNFbvo; aw. by rewrite (CNFq_p3 (proj1 h0) (cltS NS0)) (oprod1r oc). - by move => o /clt0. move => n nN Hrec ax. move: (CNFp_p2 ax (NS_succ nN) (@succ_nz n)) => [pa1 pa2 ->]. move: (Hrec (CNFb_p5 (NS_succ nN) ax)) => [p [ax3 -> h1 h3]] {Hrec}. set sa := _ -o _; set sb := c (csucc n). move: (proj32_1 pa1)=> osa. move/posnat_ordinalp :(pa2) => /proj1/proj32_1 osb. have of3:=(OS_succ (OS_prod2 (OS_pow OS_omega osa) osb)). pose p1 i := Yo (i = (csucc n)) (p n) (Yo (i = n) (J sa sb) (p i)). have aux: forall i, i <c csucc n -> (i <> csucc n /\ (i = n \/ (i <> n /\ i <c n))). move => i h ; split; first by exact (proj2 h). move /(cltSleP nN): h => lt1. by case: (equal_or_not i n) => hc; [left | right]. exists p1; split. + move: ax3 => [pa pb]; rewrite /p1; split; last by Ytac0. move => i /aux [ra rb]; Ytac0. case: rb=> rc; [ Ytac0; aw |case: rc=> [rc1 rc2]; Ytac0; fprops]. split; aw; fprops. + rewrite /CNFpv (CNFp_r _ nN). have ->: CNFpv1 p1 n = CNFpv1 p n. apply:(oprodf_exten nN) => i lin. move: (proj2(clt_leT lin (cleS nN))) (proj2 lin) => ha hb. by rewrite /p1 /cantor_pmon; Ytac0; Ytac0. have of1: ordinalp (oopow (P (p n)) *o Q (p n)). rewrite h3; aw. exact:(CNFq_p0 (proj1 ax) (succ_positive (csucc n))). rewrite /p1/cantor_pmon (Y_false (proj2(cltS nN))); Ytac0; Ytac0. by rewrite (oprodA of1 (OS_CNFp1 (proj1 ax3) nN)); aw. + rewrite /p1;move => i /aux [ra rb]; Ytac0; case:rb=> rb. by Ytac0; rewrite rb/sa (cpred_pr1 (CS_nat nN)). move: rb =>[rb1 rb2];Ytac0; fprops. + by rewrite /p1; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)