proposition: Lemma dominates_cadd d (T : measurableType d) (R : realType) (mu : {sigma_finite_measure set T -> \bar R}) (nu0 nu1 : {charge set T -> \bar R}) : nu0 `<< mu -> nu1 `<< mu -> cadd nu0 nu1 `<< mu.
proof: Proof. by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral