proposition: Lemma nsum_p6 f n: nat_ord_seq f -> natp n -> n_sum_from_n f n = \0o -> finite_set (nsupport f).
proof: Proof. move => ax nN rz; move: (proj1 (nsum_p5 ax nN rz)) => ms. have h : sub (nsupport f) n. move => t /Zo_P [tN fnz]. case: (NleT_el nN tN); first by move => h; case: fnz; apply: ms. by move/(NltP nN). exact: (sub_finite_set h (finite_set_nat nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)