proposition: Lemma measure_unique A : measurable A -> m1 A = m2 A.
proof: Proof. move=> mA; apply: (@g_salgebra_measure_unique _ _ _ G); rewrite -?mG//. by rewrite mG; exact: sub_sigma_algebra. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)