proposition: Lemma le_integrable f g : measurable_fun D f -> (forall x, D x -> `|f x| <= `|g x|) -> mu_int g -> mu_int f.
proof: Proof. move=> mf fg /integrableP[mfg goo]; apply/integrableP; split => //. by apply: le_lt_trans goo; apply: ge0_le_integral => //; exact: measurableT_comp. 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