proposition: Lemma nsum_ne f : nat_ord_seq f -> ~ finite_set (nsupport f) -> \0o <o n_sum f.
proof: Proof. move => axf si. apply:(all_sums_p3 axf) => allz; case: si. suff: (nsupport f) = emptyset by move ->; apply: emptyset_finite. apply/set0_P => x /Zo_P [xN xv]. have xdf: inc x (domain f) by rewrite (proj32 axf). by move: (allz x xdf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)