proposition: Lemma nsum_p10f f:nat_ord_seq f -> finite_set (nsupport f) -> n_sum f = (n_partial_sum f (nsupport f)) +o \0o.
proof: Proof. move => axf fs. have sEN: sub (nsupport f) Nat by apply: Zo_S. rewrite (osum0r (OS_nsum axf sEN)) (nsum_p1 axf). move:Nat_order_wor => [wor sr]. rewrite - sr in sEN. move:(nsum_p0 axf) => foo. have ok i: inc i (substrate Nat_order -s (nsupport f)) -> Vg f i = \0o. by rewrite sr => /setC_P [iN /Zo_P ie]; ex_middle bad; case ie. rewrite /n_partial_sum - sr; exact: (isum_p9 wor sEN foo ok). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)