fix

Author: affeldt-aist

_CoqProject

@@ -44,7 +44,7 @@ theories/convex.v
 theories/charge.v
 theories/kernel.v
 theories/prob_lang.v
-theories/wip.v
+theories/prob_lang_wip.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v

theories/wip.v renamed to theories/prob_lang_wip.v

@@ -75,7 +75,7 @@ Let mgauss01_sigma_additive : semi_sigma_additive mgauss01.
 Proof.
 move=> /= F mF tF mUF.
 rewrite /mgauss01/= integral_bigcup//=; last first.
-  split.
+  apply/integrableP; split.
     apply/EFin_measurable_fun.
     exact: measurable_funS (measurable_fun_gauss_density 0 1).
   rewrite (_ : (fun x => _) = (EFin \o gauss01_density)); last first.