proposition: Lemma lee_sum_fset_lim (R : realType) (f : (\bar R)^nat) (F : {fset nat}) (P : pred nat) : (forall i, P i -> 0%E <= f i) -> \sum_(i <- F | P i) f i <= \sum_(i <oo | P i) f i.
proof: Proof. move=> f0; pose n := (\max_(k <- F) k).+1. rewrite (le_trans (lee_sum_fset_nat F n _ _ _))//; last exact: nneseries_lim_ge. move=> k /= kF; rewrite /n big_seq_fsetE/=. by rewrite -[k]/(val [`kF]%fset) ltnS leq_bigmax. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun