proposition: Lemma ae_ge0_le_integral : {ae mu, forall x, D x -> f1 x <= f2 x} -> \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x.
proof: Proof. move=> [N [mN muN f1f2N]]; rewrite (ge0_negligible_integral _ _ _ _ muN)//. rewrite [leRHS](ge0_negligible_integral _ _ _ _ muN)//. apply: ge0_le_integral; first exact: measurableD. - by move=> t [Dt _]; exact: f10. - exact: measurable_funS mf1. - by move=> t [Dt _]; exact: f20. - exact: measurable_funS mf2. - by move=> t [Dt Nt]; move/subsetCl : f1f2N; apply. 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