proposition: Lemma ord_factor4 p n (q := fun i => odegree (odegree (p i))) (r := fun i => q (cpred (n -c i))): ord_factor_list p n -> (forall i, i <c n -> limit_ordinal (p i)) -> [/\ forall i, i <c n -> p i = oopow (oopow (q i)), CNFr_ax r n & oprodf p n = oopow (CNFrv r n)].
proof: Proof. move => h. have h0:=(ord_factor1 h). move: h => [nN axa axb] H. pose dd x := odegree (odegree x). have dd1 x: ordinalp x -> ordinalp (dd x). move => ox. set T:= OS_degree; exact: (T _ (T _ ox)). pose oo e := oopow (oopow e). have Hp x:(exists2 e, ordinalp e & x = oo e) -> x = oo (dd x). move => [e oe ->]; move:(OS_oopow oe) => ooe. by rewrite /dd/oo (odegree_opow ooe) (odegree_opow oe). have h1: forall i, i <c n -> p i = oo (dd (p i)). move => i lin; move: (limit_nonsucc' (H _ lin)) => p1. case /ord_prime_p1: (axa i lin). - by move/ord_ptypeF_prop => [hh]; case: p1. - by move/ord_ptypeI_prop => [hh]; case: p1. - by move => /Hp. have h2 i: natp i -> (csucc i) <c n -> q (csucc i) <=o q i. move => iN lin; move:(proj2 (axb i iN lin) _ (dd1 _ (h0 _ lin)) (h1 _ lin)). move => [e ea eb]; move:(proj32 ea) => oe; move:(OS_pow OS_omega oe) => ooe. by rewrite /q eb (odegree_opow ooe)(odegree_opow oe). have rp1: ord_below r n. move => i lin; rewrite /r; move:(cdiff_lt_symmetry nN lin) => lrin. exact:(dd1 _ (proj31 (H _ lrin))). have h3: CNFr_ax r n. split; [exact | move => i iN [lin nin]]; rewrite /r. move:(cdiff_pr lin) (NS_diff (csucc i) nN); set u := n -c csucc i. move => nv uN. case: (equal_or_not u \0c) => unz. case: nin; rewrite - nv unz csum0r; fprops. move: (cpred_pr uN unz) => [ha hb]. have hc: csucc (cpred u) <c n. rewrite - hb - nv csumC; apply:(csum_M0lt uN (@succ_nz _)). by move: (h2 _ ha hc);rewrite (cdiff_A1 nN iN lin) - hb. split => //. transitivity (oprodf (fun i => oo (q i)) n). by apply: (oprodf_exten nN) => i /h1. rewrite /r; move: nN rp1; rewrite/r; clear. move:n; apply:Nat_induction. by move => _; rewrite oprod_f0 CNFr_p5 oopow0. move => n nN Hrec hr. rewrite (oprod_fS _ nN). have ha: \1c +c n = csucc n by rewrite (Nsucc_rw nN) csumC. have hb: ord_below (fun i => omega0 ^o q (cpred (csucc n -c i))) (\1c +c n). by rewrite ha; move => i lin /=; apply: (OS_pow OS_omega); apply: hr. move:(osum_fA NS1 nN hb); rewrite ha /CNFrv => ->. have eq1: (omega0 ^o q (cpred (csucc n -c \0c))) = omega0 ^o (q n). by rewrite (cdiff_n0 (NS_succ nN)) (cpred_pr2 nN). have lt1: \0c <c (\1c +c n) by rewrite ha; apply: succ_positive. have op1: ordinalp (osumf (fun z : Set => omega0 ^o q (cpred (csucc n -c (z +c \1c)))) n). apply:(OS_osumf nN) => i lin; apply: hb. by rewrite csumC; apply:(csum_Meqlt NS1 lin). have hc: ord_below (fun i => q (cpred (n -c i))) n. move => i lin /=; rewrite - (cdiff_succ (CS_nat nN)(proj31_1 lin)). by apply:(hr (csucc i) (cltSS lin)). rewrite (osum_f1 (hb _ lt1)) /oopow (opow_sum OS_omega op1 (hb _ lt1)) eq1. rewrite (Hrec hc); apply: f_equal2; [apply: f_equal | done]. apply:(osumf_exten nN) => i lin /=. by rewrite - (csucc_pr4 (proj31_1 lin)) (cdiff_succ (CS_nat nN) (proj31_1 lin)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)