proposition: Lemma nsum_p7 f : nat_ord_seq f -> finite_set (nsupport f) -> exists2 n, natp n & n_sum_from_n f n = \0o.
proof: Proof. move => ax fs. have [m mN mp]: exists2 m, natp m & forall n, inc n (nsupport f) -> n <c m. have sN: sub (nsupport f) Nat by apply/Zo_S. exact:(finite_subset_Nat_bis sN fs). exists m => //. move:Nat_order_wor => [wor sr]. have ra: sub m (substrate Nat_order) by rewrite sr; apply: NS_inc_nat. have rb i: inc i (substrate Nat_order -s m) -> Vg f i = \0o. rewrite sr => /setC_P [iN im]; ex_middle bad. have: inc i (nsupport f) by apply: Zo_i. by move/mp => /(NltP mN). move: (isum_p9 wor ra (nsum_p0 ax) rb). rewrite sr - [ipartial_sum f Nat_order Nat] (nsum_p1 ax) (nsum_p2 ax mN). rewrite -/(n_partial_sum _ _ ) -/(n_sum_to_n _ _ ). rewrite - {2} (osum0r (OS_nsumb ax mN)). by move/(osum2_simpl (OS_nsumc ax mN) OS0 (OS_nsumb ax mN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)