proposition: Lemma finite_rems4 f n k a (b := CNFrv f k) (c := CNFrv f n) (a1:= CNFrv (fun i => f (i +c k)) (n -c k)): natp n -> CNFr_ax f n -> k <=c n -> k <> \0c-> ordinalp a -> (c = a +o b <-> exists d, [/\ ordinalp d, d <o (oopow (f(cpred k))) & a = a1 +o d]).
proof: Proof. move => nN axn lkn kp oa. have kN:= (NS_le_nat lkn nN). have axk: CNFr_ax f k. split; first by move => i lik;exact: (proj1 axn _ (clt_leT lik lkn)). move => i iN lik;exact: (proj2 axn _ iN (clt_leT lik lkn)). have ob: ordinalp b by apply:(OS_CNFr0 kN axk). have H m : CNFr_ax f m -> k <=c m -> natp m -> ordinalp (CNFrv (fun i => f (i +c k)) (m -c k)). move => ax' lkn' nN'. apply:(OS_osumf (NS_diff k nN')); move => i lik. move:(csum_Mlteq kN lik);rewrite (cdiff_rpr lkn') => ll. exact:(OS_pow OS_omega (proj1 ax' _ ll)). have ofb:=(proj1 axk _ (cpred_lt kN kp)). have pltb : omega0 ^o (f (cpred k)) <=o b. move:(cpred_pr kN kp)=> [sa sb]; rewrite sb in axk. rewrite /b {2} sb; exact:(CNFr_p2 sa axk). split; last first. have eq2: c = a1 +o b. move:(cdiff_pr lkn); move: (NS_diff k nN); set m:= _ -c _=> mN dv. have ax2: ord_below (fun i => omega0 ^o f i) (k +c m). rewrite dv => i /(proj1 axn) ofi; apply: (OS_pow OS_omega ofi). by move:(osum_fA kN mN ax2); rewrite dv. move => [d [od ds dv]]. rewrite eq2 dv - (osumA (H n axn lkn nN) od ob). move:(ord_negl_opow ds ofb) => na. by rewrite (ord_negl_sum' od na pltb). rewrite /c /a1; clear c a1. move: n nN axn lkn a oa. apply: Nat_induction. by move => _ /cle0 k0; case: kp. move => n nN Hrec axn lkn a oa eq. case:(finite_rems_aux nN axn oa ob eq). move => [bv asmall]. move:(proj1 (CNFr_unique axn axk (NS_succ nN) kN bv)) => nk. rewrite nk cdiff_nn /CNFrv osum_f0 - nk (cpred_pr2 nN). by exists a; split => //;rewrite osum0l. move =>[a' [oa' av eq']]. move:(cltS nN) => ltcpn. have ax := (CNFr_ax_s nN axn). have ofn :=(proj1 axn n ltcpn). have op1:= (OS_pow OS_omega ofn). case:(cle_eqVlt lkn) => lekn. have ops := (OS_CNFr0 nN (CNFr_ax_s nN axn)). move:(esym eq'); rewrite /b lekn (CNFr_rec _ nN) (osumA oa' op1 ops). move/(ord_negl_sum1 oa' op1 ops) =>[_]. rewrite /(ord_negl _ _) - (CNFr_rec f nN). rewrite -/b. move/(CNFr_unique axn ax (NS_succ nN) nN). by move => [bad _ ]; case: (proj2 ltcpn). move/(cltSleP nN):lekn => lekn. move: (Hrec ax lekn a' oa' eq') => [d [od ds ww]]. exists d; split => //. rewrite (cdiffSn nN lekn) (CNFr_rec _ (NS_diff k nN)) (cdiff_rpr lekn). by rewrite -(osumA op1 (H n ax lekn nN) od) - ww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)