proposition: Lemma indic_fubini_tonelli : \int[m1]_x F x = \int[m2]_y G y.
proof: Proof. rewrite -indic_fubini_tonelli1// -indic_fubini_tonelli2// integral_indic//=. rewrite integral_indic//= !setIT. by apply: product_measure_unique => //= ? ? ? ?; rewrite product_measure2E. 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