proposition: Lemma nsum_p8 f : nat_ord_seq f -> ~ finite_set (nsupport f) -> exists2 n, natp n & n_sum_from_n f n = least_rem (n_sum f).
proof: Proof. move => axf si. move:(nsum_ne axf si) => sp. move: (least_rem_p1 sp) (least_rem_p3 sp); set b := least_rem _. move => [bp [a oa sv]] inb. move:(bp) => [[_ ob _] /nesym bnz]. move:Nat_order_wor => [wor sr]. move /nsum_p0: (axf) => fp. have sv1: ipartial_sum f Nat_order (substrate Nat_order) = a +o b. by rewrite sr - /(n_partial_sum _ _)- (nsum_p1 axf) sv. move:(isum_p6 wor fp oa ob bnz sv1) => [n [u [v ]]]; rewrite sr. move => [nN ou ov vp [eqa eqb eqc]]; exists (csucc n); first by apply: NS_succ. move: eqc. rewrite -/(n_partial_sum _ _). have ->: (Zo Nat [eta glt Nat_order n]) = Nat -s (csucc n). set_extens t. move =>/ Zo_P [tN [/Nat_order_leP [ha hb hx]] hd]. by apply/setC_P; split => //; move/(NleP nN) => he; case: hd; apply: cleA. move => /setC_P [tN /(NleP nN) ltn]. case:(NleT_el tN nN) => // - [lnt nnt]; apply:(Zo_i tN). by split => //; apply/Nat_order_leP. rewrite -/(n_sum_from_n _ _). set c := n_sum_from_n f (csucc n) => eq4. have oc: ordinalp c by apply: (OS_nsumc axf (NS_succ nN)). case: (indecomp_pr ov oc inb (esym eq4)) => //. rewrite eq4 => /esym eq5; move: (osum2_a_ab ov oc eq5) => cz. case: si; apply:(nsum_p6 axf (NS_succ nN) cz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)