minor simplification

CHANGELOG_UNRELEASED.md

@@ -77,6 +77,9 @@
     the previous definition can be recovered with the lemma
     `null_dominatesP`
 
+- in `lebesgue_integral_monotone_convergence.v`:
+  + lemma `ge0_le_integral` (remove superfluous hypothesis)
+
 ### Renamed
 
 - in `probability.v`:

theories/charge.v

@@ -1428,7 +1428,6 @@ move=> mA; apply: ereal_nondecreasing_is_cvgn => a b ab.
 apply: ge0_le_integral => //.
 - by move=> ? ?; exact: max_approxRN_seq_ge0.
 - by apply: measurable_funS (measurable_max_approxRN_seq a).
-- by move=> ? ?; exact: max_approxRN_seq_ge0.
 - exact: measurable_funS (measurable_max_approxRN_seq b).
 - by move=> x _; exact: max_approxRN_seq_nd.
 Qed.
@@ -1587,7 +1586,6 @@ apply/andP; split; last first.
 apply: ge0_le_integral => //.
 - by move=> x _; exact: approxRN_seq_ge0.
 - exact: measurable_approxRN_seq.
-- by move=> ? *; exact: max_approxRN_seq_ge0.
 - exact: measurable_max_approxRN_seq.
 - by move=> ? _; exact: max_approxRN_seq_ge.
 Qed.

theories/gauss_integral.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
@@ -297,7 +297,6 @@ rewrite fine_le//.
 apply: ge0_le_integral => //=.
 - by move=> y _; rewrite lee_fin u_ge0.
 - by apply/measurable_EFinP => /=; apply/measurable_funTS; exact: measurable_u.
-- by move=> y _; rewrite lee_fin expR_ge0.
 - by move=> y _; rewrite lee_fin u_gauss_fun.
 Qed.
 

theories/hoelder.v

@@ -604,7 +604,6 @@ move=> mf mg.
 rewrite !Lnorm1 -ge0_integralD//=; [|by do 2 apply: measurableT_comp..].
 rewrite ge0_le_integral//.
 - by do 2 apply: measurableT_comp => //; exact: measurable_funD.
-- by move=> x _; rewrite adde_ge0.
 - by apply/measurableT_comp/measurable_funD; exact/measurableT_comp.
 - by move=> x _; rewrite lee_fin ler_normD.
 Qed.
@@ -1135,7 +1134,6 @@ rewrite gt0_ler_poweR//.
 - rewrite ge0_le_integral//.
   + apply: measurableT_comp => //; apply/measurable_EFinP.
     exact: measurable_funX.
-  + by move=> x _; rewrite lee_fin powR_ge0.
   + apply/measurable_EFinP.
     apply/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R) => //.
     exact/measurableT_comp.

theories/kernel.v

@@ -678,7 +678,6 @@ rewrite (_ : (fun x => _) =
     apply: ge0_le_integral => //.
     - by move=> y _; rewrite lee_fin.
     - exact/measurable_EFinP/measurableT_comp.
-    - by move=> y _; rewrite lee_fin.
     - exact/measurable_EFinP/measurableT_comp.
     - by move=> y _; rewrite lee_fin; exact/lefP/ndk_.
   rewrite -monotone_convergence//.
@@ -1249,7 +1248,6 @@ transitivity (\int[l x]_y lim ((\int[k (x, y)]_z (f_ n z)%:E) @[n --> \oo])).
   - move=> y _ a b ab; apply: ge0_le_integral => //.
     + by move=> z _; rewrite lee_fin.
     + exact/measurable_EFinP.
-    + by move=> z _; rewrite lee_fin.
     + exact/measurable_EFinP.
     + by move=> z _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first.

theories/lebesgue_integral_theory/giry.v

@@ -266,7 +266,6 @@ rewrite (@le_trans _ _ (\int[M]_x `|giry_ev x [set: T]|))//; last first.
   by apply/aeW => x _; rewrite gee0_abs// sprobability_setT.
 rewrite ge0_le_integral//=.
 - exact: measurable_giry_ev.
-- by move=> x _; rewrite abse_ge0.
 - by apply: measurableT_comp => //; exact: measurable_giry_ev.
 - by move=> x _; rewrite gee0_abs.
 Qed.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -90,7 +90,6 @@ have h1 : mu.-integrable D f <-> mu.-integrable D (f \_ (~` N)).
     (\int[mu]_(x in D) (`|(f \_ (~` N)) x| + `|(f \_ N) x|))).
     apply: ge0_le_integral => //.
     - by apply: measurableT_comp => //; exact: emeasurable_funD.
-    - by move=> ? ?; exact: adde_ge0.
     - by apply: emeasurable_funD; exact: measurableT_comp.
     - by move=> *; rewrite lee_abs_add.
   rewrite ge0_integralD//; [|exact: measurableT_comp..].
@@ -180,7 +179,6 @@ move=> /integrableP[mf foo] /integrableP[mg goo]; apply/integrableP; split.
 apply: (@le_lt_trans _ _ (\int[mu]_(x in D) (`|f x| + `|g x|))).
   apply: ge0_le_integral => //.
   - by apply: measurableT_comp => //; exact: emeasurable_funD.
-  - by move=> ? ?; apply: adde_ge0.
   - by apply: emeasurable_funD; apply: measurableT_comp.
   - by move=> *; exact: lee_abs_add.
 by rewrite ge0_integralD //; [exact: lte_add_pinfty| exact: measurableT_comp..].
@@ -1028,11 +1026,10 @@ have muE j : mu (E j) = 0.
   apply: (@le_trans _ _ (j.+1%:R%:E * \int[mu]_(x in E j) j.+1%:R^-1%:E)).
     by rewrite integral_cst// muleA -EFinM divff// mul1e.
   rewrite lee_pmul//; first exact: integral_ge0.
-  apply: ge0_le_integral => //; [| |by move=> x []].
-  - by move=> x [_/=]; exact: le_trans.
-  - apply: emeasurable_funB.
-    + by apply: measurable_funS msf => //; exact: subIsetl.
-    + by apply: measurable_funS msg => //; exact: subIsetl.
+  apply: ge0_le_integral => //; last by move=> x [].
+  apply: emeasurable_funB.
+  - by apply: measurable_funS msf => //; exact: subIsetl.
+  - by apply: measurable_funS msg => //; exact: subIsetl.
 have nd_E : {homo E : n0 m / (n0 <= m)%N >-> (n0 <= m)%O}.
   move=> i j ij; apply/subsetPset => x [Dx /= ifg]; split => //.
   by move: ifg; apply: le_trans; rewrite lee_fin lef_pV2// ?posrE// ler_nat.

theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v

@@ -144,7 +144,6 @@ exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans.
   apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //.
   - apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //.
     exact: measurable_funB.
-  - by move=> z _; rewrite adde_ge0.
   - apply: measurableT_comp => //; apply: measurable_funD;
       apply: (measurable_funS mE (@subset_refl _ E));
       (apply: measurableT_comp => //);
@@ -406,7 +405,6 @@ rewrite lee_pmul2l//; last 2 first.
 rewrite -ge0_integralD//=; [|by do 2 apply: measurableT_comp..].
 apply: ge0_le_integral => //=.
 - by do 2 apply: measurableT_comp => //; exact: measurable_funD.
-- by move=> /= x _; exact: adde_ge0.
 - by apply: measurableT_comp => //; apply: measurable_funD => //;
     exact: measurableT_comp.
 - by move=> /= x _; exact: ler_normD.
@@ -682,7 +680,6 @@ rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x t) e%:E))//; last first.
 apply: ge0_le_integral => //=; first exact: measurable_ball.
 - by do 2 apply: measurableT_comp => //=; apply: measurable_funB;
     [exact: measurable_funS mUf|exact: measurable_cst].
-- by move=> y _; rewrite lee_fin.
 - move=> y xry; rewrite lee_fin distrC fx'//=; apply: (lt_le_trans xry).
   by near: t; exact: nbhs0_ltW.
 Unshelve. all: by end_near. Qed.
@@ -719,7 +716,6 @@ rewrite (@le_trans _ _ (\int[mu]_(y in ball x t) e%:E))//.
   - exact: measurable_ball.
   - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //.
     by apply: measurable_funS mUf => //; apply: lxU => //=.
-  - by move=> y xty; rewrite lee_fin ltW.
   - move=> y xty; rewrite lee_fin distrC fx'//; apply: (lt_le_trans xty).
     by near: t; exact: nbhs0_ltW.
 rewrite integral_cst//=; last exact: measurable_ball.
@@ -815,7 +811,6 @@ apply: (@le_trans _ _ ((mu (ball x r))^-1 *
     + exact: measurable_ball.
     + do 2 apply: measurableT_comp => //=; apply: measurable_funB => //.
       exact: measurableT_comp.
-    + by move=> *; rewrite adde_ge0.
     + apply: emeasurable_funD => //; do 2 apply: measurableT_comp => //.
       exact: measurable_funS mf.
   by move=> /= y xry; rewrite -EFinD lee_fin// ler_normB.

theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v

@@ -332,7 +332,6 @@ rewrite !ger0_norm ?fine_ge0 ?integral_ge0 ?fine_le//.
 - by apply: integrable_fin_num => //; exact: integrableD.
 - apply: ge0_le_integral => //.
   + by apply: measurableT_comp => //; case/integrableP: (mfpn n).
-  + by move=> x Ex; rewrite adde_ge0.
   + by apply: emeasurable_funD; [move: mfp | move: mfn]; case/integrableP.
   + by move=> ? ?; rewrite fpn; exact: lee_abs_sub.
   + by move=> x Ex; rewrite adde_ge0.

theories/lebesgue_integral_theory/lebesgue_integral_fubini.v

@@ -763,7 +763,6 @@ rewrite -monotone_convergence => [|//|||]; first exact: eq_integral.
 - move=> x /= _ a b ab; apply: ge0_le_integral => //.
   + by move=> y _; rewrite lee_fin; exact: fun_ge0.
   + exact/measurable_EFinP/measurableT_comp.
-  + by move=> *; rewrite lee_fin; exact: fun_ge0.
   + exact/measurable_EFinP/measurableT_comp.
   + by move=> y _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 Qed.
@@ -796,7 +795,6 @@ rewrite -monotone_convergence => [|//|||]; first exact: eq_integral.
 - move=> y /= _ a b ab; apply: ge0_le_integral => //.
   + by move=> x _; rewrite lee_fin fun_ge0.
   + exact/measurable_EFinP/measurableT_comp.
-  + by move=> *; rewrite lee_fin fun_ge0.
   + exact/measurable_EFinP/measurableT_comp.
   + by move=> x _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 Qed.
@@ -861,7 +859,6 @@ have : m1.-integrable setT (fun x => \int[m2]_y `|f (x, y)|).
   apply/integrableP; split; first exact/measurable_fun1.
   rewrite (le_lt_trans _  ((integrable12ltyP mf).1 imf))// ge0_le_integral //.
   - by apply: measurableT_comp => //; exact: measurable_fun1.
-  - by move=> *; exact: integral_ge0.
   - exact: measurable_fun1.
   - by move=> *; rewrite gee0_abs//; exact: integral_ge0.
 move/integrable_ae => /(_ measurableT); apply: filterS => x /= /(_ I) im2f.
@@ -876,7 +873,6 @@ have : m2.-integrable setT (fun y => \int[m1]_x `|f (x, y)|).
   apply/integrableP; split; first exact/measurable_fun2.
   rewrite (le_lt_trans _ ((integrable21ltyP mf).1 imf))// ge0_le_integral //.
   - by apply: measurableT_comp => //; exact: measurable_fun2.
-  - by move=> *; exact: integral_ge0.
   - exact: measurable_fun2.
   - by move=> *; rewrite gee0_abs//; exact: integral_ge0.
 move/integrable_ae => /(_ measurableT); apply: filterS => x /= /(_ I) im2f.
@@ -918,16 +914,15 @@ apply/integrableP; split=> //.
 apply: le_lt_trans ((integrable12ltyP mf).1 imf).
 apply: ge0_le_integral; [by []|by []|..].
 - by apply: measurableT_comp; last apply: measurable_Fplus.
-- by move=> x _; exact: integral_ge0.
 - exact: measurable_fun1.
 - move=> x _; apply: le_trans.
     apply: le_abse_integral => //; apply: measurableT_comp => //.
     exact: measurable_funepos.
   apply: ge0_le_integral => //.
-  - apply: measurableT_comp => //.
+  + apply: measurableT_comp => //.
     by apply: measurableT_comp => //; exact: measurable_funepos.
-  - by apply: measurableT_comp => //; exact/measurableT_comp.
-  - by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl.
+  + by apply: measurableT_comp => //; exact/measurableT_comp.
+  + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl.
 Qed.
 
 Let integrable_Fminus : m1.-integrable setT Fminus.
@@ -936,7 +931,6 @@ apply/integrableP; split=> //.
 apply: le_lt_trans ((integrable12ltyP mf).1 imf).
 apply: ge0_le_integral; [by []|by []|..].
 - exact: measurableT_comp.
-- by move=> *; exact: integral_ge0.
 - exact: measurable_fun1.
 - move=> x _; apply: le_trans.
     apply: le_abse_integral => //; apply: measurableT_comp => //.
@@ -980,23 +974,21 @@ Let integrable_Gplus : m2.-integrable setT Gplus.
 Proof.
 apply/integrableP; split=> //; apply: le_lt_trans ((integrable21ltyP mf).1 imf).
 apply: ge0_le_integral; [by []|by []|exact: measurableT_comp|..].
-- by move=> *; exact: integral_ge0.
 - exact: measurable_fun2.
 - move=> y _; apply: le_trans.
     apply: le_abse_integral => //; apply: measurableT_comp => //.
     exact: measurable_funepos.
   apply: ge0_le_integral => //.
-  - apply: measurableT_comp => //.
+  + apply: measurableT_comp => //.
     by apply: measurableT_comp => //; exact: measurable_funepos.
-  - by apply: measurableT_comp => //; exact: measurableT_comp.
-  - by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl.
+  + by apply: measurableT_comp => //; exact: measurableT_comp.
+  + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl.
 Qed.
 
 Let integrable_Gminus : m2.-integrable setT Gminus.
 Proof.
 apply/integrableP; split=> //; apply: le_lt_trans ((integrable21ltyP mf).1 imf).
 apply: ge0_le_integral; [by []|by []|exact: measurableT_comp|..].
-- by move=> *; exact: integral_ge0.
 - exact: measurable_fun2.
 - move=> y _; apply: le_trans.
     apply: le_abse_integral => //; apply: measurableT_comp => //.

theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v

@@ -87,7 +87,6 @@ Variable mu : {measure set T -> \bar R}.
 Variables (D : set T) (mD : measurable D) (f1 f2 : T -> \bar R).
 Hypothesis f10 : forall x, D x -> 0 <= f1 x.
 Hypothesis mf1 : measurable_fun D f1.
-Hypothesis f20 : forall x, D x -> 0 <= f2 x.
 Hypothesis mf2 : measurable_fun D f2.
 
 Import HBNNSimple.
@@ -98,7 +97,8 @@ Proof.
 move=> f12; rewrite !(integral_mkcond D).
 set h1 := f1 \_ D; set h2 := f2 \_ D.
 have h10 x : 0 <= h1 x by apply: erestrict_ge0.
-have h20 x : 0 <= h2 x by apply: erestrict_ge0.
+have h20 x : 0 <= h2 x.
+  by apply: erestrict_ge0 => // t /[dup] Dt /f12; apply: le_trans; exact: f10.
 have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1.
 have mh2 : measurable_fun setT h2 by exact/(measurable_restrictT _ _).1.
 have h12 x : h1 x <= h2 x by apply: lee_restrict.
@@ -256,8 +256,6 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
     by move=> *; exact: nd_g.
   have ub n : \int[mu]_x g n x <= \int[mu]_x f x.
     apply: ge0_le_integral => //.
-    - move=> x _; apply: lime_ge => //.
-      by apply: nearW => k; exact/g0.
     - apply: emeasurable_fun_cvg mg _ => x _.
       exact: ereal_nondecreasing_is_cvgn.
     - move=> x Dx; apply: lime_ge => //.
@@ -280,7 +278,7 @@ Lemma cvg_monotone_convergence :
   \int[mu]_(x in D) g' n x @[n \oo] --> \int[mu]_(x in D) f' x.
 Proof.
 rewrite monotone_convergence; apply: ereal_nondecreasing_is_cvgn => m n mn.
-by apply: ge0_le_integral => // t Dt; [exact: g'0|exact: g'0|exact: nd_g'].
+by apply: ge0_le_integral => // t Dt; [exact: g'0|exact: nd_g'].
 Qed.
 
 End monotone_convergence_theorem.
@@ -306,7 +304,7 @@ rewrite limn_einf_lim monotone_convergence //; last first.
   by exists p => //=; rewrite (leq_trans mn).
 apply: lee_lim.
 - apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
-  apply: ge0_le_integral => //; [exact: g0| exact: mg| exact: g0| exact: mg|].
+  apply: ge0_le_integral => //; [exact: g0| exact: mg| exact: mg|].
   move=> x Dx; apply: ereal_inf_le_tmp => _ [n /= bn <-].
   by exists n => //=; rewrite (leq_trans ab).
 - apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
@@ -316,7 +314,7 @@ apply: lee_lim.
   have : forall n p, (p >= n)%N ->
       \int[mu]_(x in D) g n x <= einfs (fun k => \int[mu]_(x in D) f k x) n.
     move=> n p np; apply: le_ereal_inf_tmp => /= _ [k /= nk <-].
-    apply: ge0_le_integral => //; [exact: g0|exact: mg|exact: f0|].
+    apply: ge0_le_integral => //; [exact: g0|exact: mg|].
     by move=> x Dx; apply: ereal_inf_lbound; exists k.
   exact.
 Qed.

theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v

@@ -394,14 +394,16 @@ Proof.
 move=> f0; pose f_ := nnsfun_approx mD mf.
 transitivity (limn (fun n => \int[mscale k m]_(x in D) (f_ n x)%:E)).
   rewrite -monotone_convergence//=.
-  - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=; exact: cvg_nnsfun_approx.
+  - apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=.
+    exact: cvg_nnsfun_approx.
   - by move=> n; apply: measurableT_comp => //; exact: measurable_funTS.
   - by move=> n x _; rewrite lee_fin.
   - by move=> x _ a b ab; rewrite lee_fin//; exact/lefP/nd_nnsfun_approx.
 rewrite (_ : \int[m]_(x in D) _ =
     limn (fun n => \int[m]_(x in D) (f_ n x)%:E)); last first.
   rewrite -monotone_convergence//=.
-  - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
+  - apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //.
+    exact: cvg_nnsfun_approx.
   - by move=> n; exact/measurable_EFinP/measurable_funTS.
   - by move=> n x _; rewrite lee_fin.
   - by move=> x _ a b ab; rewrite lee_fin//; exact/lefP/nd_nnsfun_approx.
@@ -410,7 +412,6 @@ rewrite -limeMl//.
 apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //.
 - by move=> x _; rewrite lee_fin.
 - exact/measurable_EFinP/measurable_funTS.
-- by move=> x _; rewrite lee_fin.
 - exact/measurable_EFinP/measurable_funTS.
 - by move=> x _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 Qed.
@@ -711,7 +712,7 @@ have f_ge0 n x : D x -> 0 <= (f_ n x)%:E by move=> Dx; rewrite lee_fin.
 have cvg_f_ (m : {measure set T -> \bar R}) :
     cvgn (fun x => \int[m]_(x0 in D) (f_ x x0)%:E).
   apply: ereal_nondecreasing_is_cvgn => a b ab.
-  apply: ge0_le_integral => //; [exact: f_ge0|exact: f_ge0|].
+  apply: ge0_le_integral => //; first exact: f_ge0.
   by move=> t Dt; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 transitivity (limn (fun n =>
     \int[measure_add (msum m_ N) (m_ N)]_(x in D) (f_ n x)%:E)).
@@ -818,7 +819,6 @@ apply: lee_nneseries => [n _ _|n _].
 rewrite [leRHS]integral_mkcond; apply: ge0_le_integral => //.
 - by move=> x _; rewrite lee_fin.
 - exact/measurable_EFinP.
-- by move=> x _; rewrite erestrict_ge0.
 - exact/(measurable_restrictT _ mD).
 Qed.
 
@@ -1397,7 +1397,6 @@ rewrite [leRHS](ge0_negligible_integral _ _ _ _ muN)//.
 apply: ge0_le_integral; first exact: measurableD.
 - by move=> t [Dt _]; exact: f10.
 - exact: measurable_funS mf1.
-- by move=> t [Dt _]; exact: f20.
 - exact: measurable_funS mf2.
 - by move=> t [Dt Nt]; move/subsetCl : f1f2N; exact.
 Qed.
@@ -1431,7 +1430,6 @@ move=> mg a0; have ? : measurable (D `&` [set x | (a%:E <= `|g x|)%E]).
 apply: (@le_trans _ _ (\int[mu]_(x in D `&` [set x | `|g x| >= a%:E]) f `|g x|)).
   rewrite -integral_cst//; apply: ge0_le_integral => //.
   - by move=> x _ /=; rewrite f0 // lee_fin ltW.
-  - by move=> x _ /=; rewrite f0.
   - apply: measurableT_comp => //; apply: measurableT_comp => //.
     exact: measurable_funS mg.
   - by move=> x /= [Dx]; apply: f_nd;
@@ -1638,7 +1636,7 @@ exact: ge0_nondecreasing_set_nondecreasing_integral.
 Qed.
 
 Lemma le0_nondecreasing_set_cvg_integral :
- \int[mu]_(x in F i) f x @[i --> \oo] --> \int[mu]_(x in \bigcup_i F i) f x.
+  \int[mu]_(x in F i) f x @[i --> \oo] --> \int[mu]_(x in \bigcup_i F i) f x.
 Proof.
 apply/cvgeNP; rewrite -integralN/=; last first.
   apply: fin_num_adde_defr; rewrite integral0_eq// => x [n _ Fnx].

theories/pi_irrational.v

@@ -1,3 +1,4 @@
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From mathcomp Require Import functions cardinality fsbigop interval_inference.
@@ -339,8 +340,6 @@ apply/andP; split.
     apply: ge0_le_integral => //=.
     - exact: measurable_closed_ball.
     - by move=> x _; rewrite lee_fin ltW.
-    - move=> x /small_ballS/= /[!in_itv]/= /andP[x0 xpi].
-      by rewrite fsin_ge0// (ltW x0)/= ltW.
     - case/integrableP : (integrable_fsin n) => + _.
       apply: measurable_funS => // x ix.
       exact: subset_itv_oo_cc (small_ballS ix).