proposition: Lemma ge0_integral_count (a : nat -> \bar R) : (forall k, 0 <= a k) -> \int[counting]_t (a t) = \sum_(k <oo) (a k).
proof: Proof. move=> sa. transitivity (\int[mseries (fun n => [the measure _ _ of \d_ n]) O]_t a t). congr (integral _ _ _); apply/funext => A. by rewrite /= counting_dirac. rewrite (@ge0_integral_measure_series _ _ R (fun n => [the measure _ _ of \d_ n]) setT)//=. by apply: eq_eseriesr=> i _; rewrite integral_dirac//= diracT mul1e. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun