proposition: Lemma eseries_pred0 P : P =1 xpred0 -> \sum_(i <oo | P i) f i = 0.
proof: Proof. move=> P0; rewrite (_ : (fun _ => _) = fun=> 0) ?lim_cst// funeqE => n. by rewrite big1 // => i; rewrite P0. 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