diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3bb41568dc..1c313206f6 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -60,6 +60,11 @@
 - in `constructive_ereal.v`:
   + lemma `mulN1e`
 
+- in `measurable_realfun.v`:
+  + generalized and renamed:
+    * `measurable_fun_itv_bndo_bndc` -> `measurable_fun_itv_bndo_bndcP`
+    * `measurable_fun_itv_obnd_cbnd` -> `measurable_fun_itv_obnd_cbndP`
+
 ### Renamed
 
 - in `lebesgue_stieltjes_measure.v`:
diff --git a/theories/ftc.v b/theories/ftc.v
index 95bb5fe753..4abdd3a676 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -684,7 +684,7 @@ transitivity (\sum_(0 <= i <oo) ((F (a + i.+1%:R))%:E - (F (a + i%:R))%:E)).
     by rewrite lee_fin; exact: f_ge0.
   apply: eq_eseriesr => n _.
   rewrite seqDUE/= integral_itv_obnd_cbnd; last first.
-    apply: measurable_fun_itv_bndo_bndc.
+    apply/measurable_fun_itv_bndo_bndcP.
     apply: open_continuous_measurable_fun => //.
     move: cf => /continuous_within_itvcyP[cf _] x.
     rewrite inE/= in_itv/= => /andP[anx _].
@@ -1284,12 +1284,12 @@ Proof.
 move=> decrF cdF /cvg_ex[/= dFa cdFa] /cvg_ex[/= dFoo cdFoo].
 move=> [dF cFa] Fny /continuous_within_itvNycP[cG cGFa] G0.
 have mG n : measurable_fun `](F (a + n.+1%:R)), (F a)] G.
-  apply: measurable_fun_itv_bndo_bndc.
+  apply/measurable_fun_itv_bndo_bndcP.
   apply: open_continuous_measurable_fun; first exact: interval_open.
   move=> x; rewrite inE/= in_itv/= => /andP[_ xFa].
   by apply: cG; rewrite in_itv.
 have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R.
-  apply: measurable_fun_itv_obnd_cbnd.
+  apply/measurable_fun_itv_obnd_cbndP.
   apply: open_continuous_measurable_fun; first exact: interval_open.
   move=> x; rewrite inE/= in_itv/= => /andP[ax _].
   apply: continuousM; last first.
@@ -1391,7 +1391,7 @@ transitivity (limn (fun n =>
 apply: congr_lim; apply/funext => -[|n].
   by rewrite addr0 set_itvco0 set_itvoo0 !integral_set0.
 rewrite integral_itv_bndo_bndc; last first.
-  apply: measurable_fun_itv_obnd_cbnd; apply: measurable_funS (mG n) => //.
+  apply/measurable_fun_itv_obnd_cbndP; apply: measurable_funS (mG n) => //.
   by apply: subset_itvl; rewrite bnd_simp.
 rewrite integration_by_substitution_decreasing.
 - rewrite integral_itv_bndo_bndc// ?integral_itv_obnd_cbnd//.
@@ -1683,7 +1683,7 @@ rewrite -[RHS]integral_itv_obnd_cbnd; last first.
   apply: (@measurable_comp _ _ _ _ _ _ `]-oo, b]) => //=.
     rewrite opp_itv_bndy opprK/=.
     by apply: subset_itvl; rewrite bnd_simp.
-  apply: measurable_fun_itv_bndo_bndc; apply: measurable_funM => //.
+  apply/measurable_fun_itv_bndo_bndcP; apply: measurable_funM => //.
   - apply: (@measurable_comp _ _ _ _ _ _ `]-oo, F b[) => //=.
     move=> x/= [r]; rewrite in_itv/= => rb <-{x}.
     by rewrite in_itv/= ndF ?in_itv//= ltW.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
index aa1154cbc1..f40215d24a 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
@@ -1541,7 +1541,7 @@ have [xy|yx _|-> _] := ltgtP x y; last 2 first.
 move=> mf.
 transitivity (\int[mu]_(z in [set` Interval (BSide b0 x) (BLeft y)]) (f z)%:E).
   case: b1 => //; rewrite -integral_itv_bndo_bndc//.
-  by case: b0 => //; exact: measurable_fun_itv_obnd_cbnd.
+  by case: b0 => //; exact/measurable_fun_itv_obnd_cbndP.
 by case: b0 => //; rewrite -integral_itv_obnd_cbnd.
 Qed.
 
diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v
index 53af2179c0..6f454af1f2 100644
--- a/theories/measurable_realfun.v
+++ b/theories/measurable_realfun.v
@@ -183,37 +183,30 @@ End puncture_ereal_itv.
 Section salgebra_R_ssets.
 Variable R : realType.
 
-Lemma measurable_fun_itv_bndo_bndc (a : itv_bound R) (b : R)
-    (f : R -> R) :
-  measurable_fun [set` Interval a (BLeft b)] f ->
+Lemma measurable_fun_itv_bndo_bndcP (a : itv_bound R) (b : R) (f : R -> R) :
+  measurable_fun [set` Interval a (BLeft b)] f <->
   measurable_fun [set` Interval a (BRight b)] f.
 Proof.
-have [ab|ab] := leP a (BLeft b).
-- move: a => [a0 a|[|//]] in ab *;
-    move=> mf; rewrite -setUitv1//; apply/measurable_funU => //;
-    by split => //; exact: measurable_fun_set1.
-- move: a => [[|] a|[|]//] in ab *; rewrite bnd_simp in ab.
-  + move=> _; rewrite set_itv_ge// ?bnd_simp -?ltNge//.
-    exact: measurable_fun_set0.
-  + move=> _; rewrite set_itv_ge// ?bnd_simp -?leNgt//.
-    exact: measurable_fun_set0.
+split; [have [ab ?|ab _] := leP a (BLeft b) |have [ab _|ab] := leP (BLeft b) a].
+- rewrite -setUitv1//; apply/measurable_funU => //; split => //.
+  exact: measurable_fun_set1.
+- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0.
+- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0.
+- by rewrite -setUitv1 ?ltW// => /measurable_funU[].
 Qed.
 
-Lemma measurable_fun_itv_obnd_cbnd (a : R) (b : itv_bound R)
-    (f : R -> R) :
-  measurable_fun [set` Interval (BRight a) b] f ->
+Lemma measurable_fun_itv_obnd_cbndP (a : R) (b : itv_bound R) (f : R -> R) :
+  measurable_fun [set` Interval (BRight a) b] f <->
   measurable_fun [set` Interval (BLeft a) b] f.
 Proof.
-have [ab|ab] := leP (BRight a) b.
-- move: b => [[|] b|[//|]] in ab *;
-    move=> mf; rewrite -setU1itv//; apply/measurable_funU => //;
-    by split => //; exact: measurable_fun_set1.
-- move: b => [[|] b|[|//]] in ab *; rewrite bnd_simp in ab.
-  + move=> _; rewrite set_itv_ge// ?bnd_simp -?leNgt//.
-    exact: measurable_fun_set0.
-  + move=> _; rewrite set_itv_ge// ?bnd_simp -?ltNge//.
-    exact: measurable_fun_set0.
-  + by move=> _; rewrite set_itv_ge//=; exact: measurable_fun_set0.
+split; [have [ab mf|ab _] := leP (BRight a) b|
+        have [ab _|ab] := leP b (BRight a)].
+- rewrite -setU1itv//; apply/measurable_funU => //; split => //.
+  exact: measurable_fun_set1.
+- rewrite set_itv_ge; first exact: measurable_fun_set0.
+  by rewrite -leNgt; case: b ab => -[].
+- by rewrite set_itv_ge// -?leNgt//; exact: measurable_fun_set0.
+- by rewrite -setU1itv ?ltW// => /measurable_funU[].
 Qed.
 
 #[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_obnd_cbnd` instead")]
@@ -223,9 +216,9 @@ Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) :
 Proof.
 move: b0 b1 => [|] [|]//.
 - by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
-- exact: measurable_fun_itv_obnd_cbnd.
+- by move/measurable_fun_itv_obnd_cbndP.
 - move=> mf.
-  have : measurable_fun `[x, y] f by exact: measurable_fun_itv_obnd_cbnd.
+  have : measurable_fun `[x, y] f by exact/measurable_fun_itv_obnd_cbndP.
   by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
 Qed.
 
@@ -236,10 +229,10 @@ Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) :
 Proof.
 move: b0 b1 => [|] [|]//.
 - move=> mf.
-  have : measurable_fun `[x, y] f by exact: measurable_fun_itv_bndo_bndc.
+  have : measurable_fun `[x, y] f by exact/measurable_fun_itv_bndo_bndcP.
   by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
 - by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
-- exact: measurable_fun_itv_bndo_bndc.
+- by move/measurable_fun_itv_bndo_bndcP.
 Qed.
 
 Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) :
@@ -247,11 +240,11 @@ Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) :
   measurable_fun `[x, y] f.
 Proof.
 move: b0 b1 => [|] [|]//.
-- exact: measurable_fun_itv_bndo_bndc.
+- by move/measurable_fun_itv_bndo_bndcP.
 - move=> mf.
-  have : measurable_fun `[x, y[ f by exact: measurable_fun_itv_obnd_cbnd.
-  exact: measurable_fun_itv_bndo_bndc.
-- exact: measurable_fun_itv_obnd_cbnd.
+  have : measurable_fun `[x, y[ f by exact/measurable_fun_itv_obnd_cbndP.
+  by move/measurable_fun_itv_bndo_bndcP.
+- by move/measurable_fun_itv_obnd_cbndP.
 Qed.
 
 HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)).