proposition: Lemma indic_fubini_tonelli_FE : F = m2 \o xsection A.
proof: Proof. rewrite funeqE => x; rewrite /= -(setTI (xsection _ _)). rewrite -integral_indic//; last exact: measurable_xsection. rewrite /F /fubini_F -(setTI (xsection _ _)). rewrite integral_setI_indic; [|exact: measurable_xsection|by []]. by apply: eq_integral => y _ /=; rewrite indicT mul1e /f !indicE mem_xsection. 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