proposition: Lemma adde_def_nneseries (R : realType) (f g : (\bar R)^nat) (P Q : pred nat) : (forall n, P n -> 0 <= f n) -> (forall n, Q n -> 0 <= g n) -> (\sum_(i <oo | P i) f i) +? (\sum_(i <oo | Q i) g i).
proof: Proof. move=> f0 g0; rewrite /adde_def !negb_and; apply/andP; split; apply/orP. - by right; apply/eqP => Qg; have := nneseries_ge0 0 g0; rewrite Qg. - by left; apply/eqP => Pf; have := nneseries_ge0 0 f0; rewrite Pf. 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