proposition: Lemma ord_factor11 p n: ofact_list_succ p n -> exists ec m, [/\ natp m, CNFp_ax ec m, oprodf p n = CNFpv ec m & ec m = J \0o (oprodf p (first_non_int p n)) ].
proof: Proof. move => [[ nN ax1 ax2] ax3]. move: (first_non_int_p1 p nN). set k:= first_non_int p n. move => [kp1 kp2]. have lekn: k <=c n. by case: kp1;[ move ->; apply:(cleR (CS_nat nN))| case; case]. have kN := NS_le_nat lekn nN. set c0 := oprodf p k. have c0N: posnatp c0. apply:(ord_factor9_aux kN kp2) => i ilk. exact: (ax3 _ (clt_leT ilk lekn)). case: kp1 => kp1. pose ec (i: Set) := J \0o c0. move: (OS_nat(proj1 c0N)) => oc. exists ec, \0c; split => //. - apply: NS0. - split; [ by move => i /clt0 | rewrite/ec;split; aww]. - rewrite /CNFpv CNFp_0/ec; aw. by rewrite oopow0 (oprod1l oc) (oprod1r oc) /c0 kp1. move: kp1 => [lkn nn]. have kv1 := (cdiff_pr (proj1 lkn)). case: (equal_or_not (n -c k) \0c) => dnz. by case: (proj2 lkn); rewrite -kv1 dnz (csum0r (CS_nat kN)). move: (cpred_pr (NS_diff k nN) dnz); set m := cpred _; move => [mN mv]. pose p' i := p (i +c k). have hb: ofact_list_succ p' (csucc m). have h0 i: i <c csucc m -> i +c k <c n. by move => link; move: (csum_Meqlt kN link); rewrite - mv kv1 csumC. split. split; [exact:(NS_succ mN) | by move => i /h0 lin; apply:ax1 |]. by move=> i iN /h0;rewrite /p' (csum_Sn _ iN);apply: (ax2 _ (NS_sum iN kN)). by move => i /h0 lin; apply:ax3. have hc : ~ natp (p' \0c) by rewrite /p' (csum0l (CS_nat kN)). move: (@ord_factor9 p' m hb mN hc) => [ec [q[r1 r2 r3 r4 r5]]]. have sqN := NS_succ r1. pose ec' i := Yo (i = (csucc q)) (J \0o c0) (ec i). have r6: CNFp_ax ec' (csucc q). rewrite/ec';split. by move => i lin; rewrite (Y_false (proj2 lin)); apply: r2. Ytac0; split; aww. have r7: oprodf p n = CNFpv ec' (csucc q). have ra: CNFpv1 ec' (csucc q) = CNFpv1 ec (csucc q). apply: (oprodf_exten sqN). by rewrite /ec'/cantor_pmon=> i /proj2 lin; Ytac0. rewrite /CNFpv ra - r3 /ec'; Ytac0; aw. rewrite oopow0 (oprod1l (OS_nat (proj1 c0N))). have obl : ord_below p (k +c (n -c k)). by rewrite kv1; move => i /(ax1); case. by rewrite /c0 -{1} kv1 (oprod_fA kN (NS_diff k nN) obl) mv. have r8: ec' (csucc q) = J \0o c0 by rewrite /ec' /=; Ytac0. by exists ec', (csucc q). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)