proposition: Lemma ord_factor6 p n k (p':= fun i => p (i +c k)): ord_factor_list p n -> ord_factor_boundary p n k -> [/\ ord_factor_list p k, ord_factor_list p' (n -c k), forall i, i<c k -> limit_ordinal (p i), forall i, i<c (n -c k) -> osuccp (p' i) & [/\ oprodf p n = (oprodf p k) *o (oprodf p' (n -c k)), exists2 e, ordinalp e & oprodf p k = oopow e & osuccp (oprodf p' (n -c k)) ] ].
proof: Proof. move => [nN axa axb] [lkn ha hb]. move:(cdiff_pr lkn); move:(NS_diff k nN) => dN dv. have kN := NS_le_nat lkn nN. have aux i: i <c n -c k -> i +c k <c n. by move => link; move: (csum_Meqlt kN link); rewrite dv csumC. have R1: ord_factor_list p k. split; first exact. move => i lin; exact:(axa _ (clt_leT lin lkn)). move => i iN lin; exact:(axb _ iN (clt_leT lin lkn)). have R2: ord_factor_list p' (n -c k). split; first exact. move => i /aux lin; exact:(axa _ lin). move => i iN /aux. rewrite/p' (csum_Sn _ iN) => lin. exact:(axb _ (NS_sum iN kN) lin). have R4: forall i, i <c n -c k -> osuccp (p' i). move => i likn; move:(aux _ likn) => ll; apply:hb ll. rewrite csumC; exact(Nsum_M0le i kN). have R5: oprodf p n = oprodf p k *o oprodf p' (n -c k). by rewrite - {1} dv (oprod_fA) //; rewrite dv; apply:ord_factor1. have R6: exists2 e : Set, ordinalp e & oprodf p k = omega0 ^o e. move: (ord_factor4 R1 ha); set f := fun i:Set => _. move => [_ resa ->]; move: (OS_CNFr0 kN resa) => oe. by exists (CNFrv f k). have R7: osuccp (oprodf p' (n -c k)). move: (n-c k) dN R4; clear; apply: Nat_induction. by move => _; exists \0o; [ exact: OS0 |rewrite oprod_f0 osucc_zero]. move => n nN Hrec hi. have h2: forall i, i <c n -> osuccp (p' i). move => i lin; exact: (hi _ (clt_ltT lin (cltS nN))). move:(hi _ (cltS nN)) (Hrec h2) => r1 r2. have oe1: ordinalp (oprodf p' n) by move: r2 =>[t ot ->];exact: (OS_succ ot). have oe2: ordinalp (p' n) by move: r1 =>[t ot ->];exact: (OS_succ ot). by rewrite (oprod_fS _ nN); apply/oprod_succP. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)