proposition: Lemma nsum_p10a f (rho := least_rem (n_sum 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 = rho /\ Vg f m <o rho.
proof: Proof. move => axf si. move: (nsum_p9 axf si); rewrite -/rho; move => [n nN np]. have rp := (proj1 (least_rem_p1 (nsum_ne axf si))). exists n => //m mN le1; move:(np m mN le1) => eq1; split => //. move: (nsum_p4 axf mN). rewrite eq1 (np _ (NS_succ mN) (cleT le1 (cleS mN))) => sc. have ox: ordinalp (Vg f m) by apply: (proj33 axf); rewrite (proj32 axf). by move: (osum_Meqlt rp ox); rewrite - sc (osum0r ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)