proposition: Lemma nsum_p10b f: nat_ord_seq f -> ~ finite_set (nsupport f) -> finite_set(n_sum_small_idx1 f).
proof: Proof. move => ha hb; move: (nsum_p10a ha hb) =>[n nN np]. rewrite/n_sum_small_idx1; set E := Zo _ _. suff: sub E n by move => h; move : (sub_finite_set h (finite_set_nat nN)). move => i /Zo_P [iN le1]; case: (NleT_el nN iN); last by move/(NltP nN). move => le2; case: (oleNgt le1 (proj2 (np i iN le2))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)