proposition: Lemma ereal_series_cond k P : \sum_(k <= i <oo | P i) f i = \sum_(i <oo | (k <= i)%N && P i) f i.
proof: Proof. apply/congr_lim/funext => n. rewrite big_nat_cond (big_nat_widenl k 0%N)//= 2!big_mkord. by apply: eq_big => //= i; rewrite andbAC ltn_ord andbT andbb. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau