proposition: Lemma nsum_p10e f (rho := (least_rem (n_sum f))): nat_ord_seq f -> ~ finite_set (nsupport f) -> n_sum f = (n_partial_sum f (n_sum_small_idx1 f)) +o rho.
proof: Proof. move => ha hb. move: (nsum_p10a ha hb) =>[n nN np]. move: (proj1 (np n nN (cleR (CS_nat nN)))); rewrite -/rho => eq1. move: (least_rem_p3 (nsum_ne ha hb)); rewrite -/rho => ri. rewrite (nsum_p2 ha nN) eq1. set E := (n_sum_small_idx1 f). have /setI2id_Pl sEn: sub E n. move => i /Zo_P [iN le1]; case: (NleT_el nN iN); last by move/(NltP nN). by move => le2; case: (oleNgt le1 (proj2 (np i iN le2))). rewrite - sEn. rewrite /n_sum_to_n /n_partial_sum. pose A m := n -s (n -c m). have Ap m : A m = Zo n (fun i => n -c m <=c i). have uN :=(NS_diff m nN). set_extens t. move => /Zo_P [tn /(NltP uN) nn]. have tN: natp t by exact: (NS_inc_nat nN tn ). by case: (NleT_el uN tN) => // ll; apply: Zo_i. by move =>/Zo_P [tn /cleNgt le]; apply: (Zo_i tn) => /(NltP uN). have ->: n = A n by rewrite /A cdiff_nn setC_0. move: (cleR (CS_nat nN)). move:Nat_order_wor => [wor sr]. move: {-3} (n) (nN); apply: Nat_induction. move => _; rewrite /A (cdiff_n0 nN) setC_v. have -> //: E \cap emptyset= emptyset. by apply/set0_P => t /setI2_P [_ /in_set0]. move => m mN Hrec ll. set v := n -c (csucc m). move: (csucc_diff nN mN ll) => sv. have vN: natp v . by apply: NS_diff. have lvb: v <c n by apply: (cdiff_ltb nN ll (@succ_nz _)). have ->: A (csucc m) = singleton v \cup (A m). rewrite ! Ap; set_extens t. move => /Zo_P [rn]; case/cle_eqVlt. rewrite /v; move ->; apply: setU2_1; fprops. by move/(cleSltP vN); rewrite sv => xx; apply: setU2_2; apply: Zo_i. case/setU2_P. move/set1_P ->; apply: Zo_i; first by apply/(NltP nN). apply: (cleR (CS_nat vN)). move => /Zo_P [tn hyp]; apply:(Zo_i tn). suff: n -c csucc m <c t by case. by apply /(cleSltP vN); rewrite - sv. move: (nsum_p0 ha) => axf. have ra: sub (singleton v) (substrate Nat_order) by move => u /set1_P ->; ue. have rb: sub (A m) (substrate Nat_order). by rewrite sr; move =>u /setC_P [/ (NS_inc_nat nN)]. have rc i j: inc i (singleton v) -> inc j (A m) -> glt Nat_order i j. rewrite Ap; move => /set1_P -> /Zo_P [jn lt]. move: (NS_inc_nat nN jn) => jN. have [qa qb] : v <c j. by apply/(cleSltP vN); rewrite - sv. split => //; apply/Nat_order_leP; split => //. have rd: inc v (substrate Nat_order) by ue. rewrite - (isum_p4 wor axf ra rb rc). have ov: ordinalp (Vg f v) by apply (proj33 ha); rewrite (proj32 ha). have orho: ordinalp rho by move: (proj32_1 (proj1 ri)). have os1: ordinalp (ipartial_sum f Nat_order (A m)) by apply: isum_p1. rewrite (isum_p3 wor axf rd). case: (inc_or_not v E) => ivE. have h: sub (singleton v) E by move => y /set1_P ->. move/ (setU2id_Pl): h => <-; rewrite - set_UI2r. have rb1: sub (E \cap A m) (substrate Nat_order). by move => t/setI2_P [_]; apply: rb. have rc1 i j: inc i (singleton v)-> inc j (E \cap (A m))-> glt Nat_order i j. by move => ii /setI2_P [_ jj]; apply: rc. have os2: ordinalp (ipartial_sum f Nat_order (E \cap A m)) by apply: isum_p1. rewrite - (isum_p4 wor axf ra rb1 rc1) (isum_p3 wor axf rd). rewrite - (osumA ov os2 orho) - (osumA ov os1 orho). by rewrite (Hrec (cleT (cleS mN) ll)). have -> : (E \cap (singleton v \cup A m)) = E \cap (A m). rewrite set_IU2r; set_extens t. case/setU2_P => // /setI2_P [iE /set1_P ee]; case: ivE; ue. by move => qa; apply: setU2_2. case: (oleT_el orho ov) => vs; first by case: ivE; apply : Zo_i. rewrite - (Hrec (cleT (cleS mN) ll)). apply: (indecomp_sier os1 ri vs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)