proposition: Lemma indic_fubini_tonelli_GE : G = m1 \o ysection A.
proof: Proof. rewrite funeqE => y; rewrite /= -(setTI (ysection _ _)). rewrite -integral_indic//; last exact: measurable_ysection. rewrite /F /fubini_F -(setTI (ysection _ _)). rewrite integral_setI_indic; [|exact: measurable_ysection|by []]. by apply: eq_integral => x _ /=; rewrite indicT mul1e /f 2!indicE mem_ysection. 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