proposition: Lemma except_in_nsum_finite2 f: nat_ord_seq f -> finite_set (except_in_nsums f).
proof: Proof. move => h; move: (except_in_nsum_finite h) =>[n nN etc]. have /sub_finite_set aux: sub (except_in_nsums f) (Nintc n). by move => t /etc/(NintcP nN). apply: aux;apply: finite_Nintcc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)