proposition: Lemma nsum_p9 f : nat_ord_seq f -> ~ finite_set (nsupport f) -> exists2 n, natp n & forall m, natp m -> n <=c m -> n_sum_from_n f m = least_rem (n_sum f).
proof: Proof. move => axf si. move:(nsum_ne axf si) => sp. move: (nsum_p8 axf si) => [n nN hc]; exists n => //. apply: Nat_induction; first by move /cle0 => <-. move => m mN Hrec /cle_eqVlt; case; first by move <-. move/(cltSleP mN) => /Hrec; rewrite (nsum_p4 axf mN). move: (least_rem_p3 sp); set b := least_rem _ => inb => eq1. have aox: ordinalp (Vg f m) by apply : (proj33 axf); rewrite (proj32 axf). have or := (OS_nsumc axf (NS_succ mN)). move: (@indecomp_pr b (Vg f m) (n_sum_from_n f (csucc m)) aox or inb eq1). case => //. rewrite - eq1 => /esym eq5; move: (osum2_a_ab aox or eq5) => cz. case: si; apply:(nsum_p6 axf (NS_succ mN) cz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)