generalize setUitv1, setU1itv, setDitv1{l,r}, and add similar lemmas (#1864)

* generalize setUitv1, setU1itv, setDitv1{l|r}; add similar lemmas

* add lteifS to mathcomp_extra and use it instead of ltrW_lteif

Author: t6s

CHANGELOG_UNRELEASED.md

@@ -3,6 +3,10 @@
 ## [Unreleased]
 
 ### Added
+- in set_interval.v
+  + lemmas `setUitv_set2`, `setDitv_set2`, `setDitvoo`, `setDitvoy`, `setDitvNyo`,
+    `setDccitv`, `setD_cbnd_bndy`, `setD_bndc_Nybnd`
+
 - in `topology_structure.v`
   + lemma `interiorS`
 
@@ -67,6 +71,9 @@
   + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`
 
 ### Changed
+- in set_interval.v
+  + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized)
+
 - in `set_interval.v`
   + `itv_is_closed_unbounded` (fix the definition)
 

classical/mathcomp_extra.v

@@ -84,6 +84,10 @@ Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) :
   #|` A| = (\sum_(i <- A) 1)%N.
 Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed.
 
+Lemma lteifS {disp : Order.disp_t} {T : porderType disp}
+  [x y : T] (C : bool) : (x < y)%O -> (x < y ?<= if C)%O.
+Proof. by case: C => //= /ltW. Qed.
+
 (**************************)
 (* MathComp 2.6 additions *)
 (**************************)

classical/set_interval.v

@@ -182,38 +182,58 @@ Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo,
 Lemma set_itvxx a : [set` Interval a a] = set0.
 Proof. by move: a => [[|] a |[|]]; rewrite !set_itvE. Qed.
 
-Lemma setUitv1 a x : (a <= BLeft x)%O ->
-  [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].
+Lemma setUitv1 a x b : (a <= BLeft x)%O ->
+  [set` Interval a (BSide b x)] `|` [set x] = [set` Interval a (BRight x)].
 Proof.
-move=> ax; apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE.
+move=> ax; case: b; last first.
+  by apply: setUidl => ? /= ->; rewrite itv_boundlr ax lexx.
+apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE.
 by rewrite (rwP eqP) (rwP orP) orbC.
 Qed.
 
-Lemma setU1itv a x : (BRight x <= a)%O ->
-  x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a].
+Lemma setU1itv a x b : (BRight x <= a)%O ->
+  x |` [set` Interval (BSide b x) a] = [set` Interval (BLeft x) a].
 Proof.
-move=> ax; apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE.
+move=> ax; case: b.
+  by apply: setUidr => ? /= ->; rewrite itv_boundlr ax lexx.
+apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE.
 by rewrite (rwP eqP) (rwP orP) orbC.
 Qed.
 
-Lemma setDitv1r a x :
-  [set` Interval a (BRight x)] `\ x = [set` Interval a (BLeft x)].
+Lemma setUitv_set2 x y b1 b2 :
+  (x <= y)%O ->
+  [set` Interval (BSide b1 x) (BSide b2 y)] `|` [set x; y] = `[x, y]%classic.
 Proof.
+rewrite le_eqVlt => /orP [/eqP->|xy].
+  by case: b1; case: b2; rewrite !set_itvE !setUid // set0U.
+rewrite setUCA setUitv1; last by case: b1; rewrite bnd_simp// ltW.
+by rewrite setU1itv// bnd_simp ltW.
+Qed.
+
+Lemma setDitv1r a x b :
+  [set` Interval a (BSide b x)] `\ x = [set` Interval a (BLeft x)].
+Proof.
+case: b; first by apply: not_setD1; rewrite /= in_itv/= ltxx andbF.
 apply/seteqP; split => [z|z] /=; rewrite !in_itv/=.
   by move=> [/andP[-> /= zx] /eqP xz]; rewrite lt_neqAle xz.
 by rewrite lt_neqAle => /andP[-> /andP[/eqP ? ->]].
 Qed.
 
-Lemma setDitv1l a x :
-  [set` Interval (BLeft x) a] `\ x = [set` Interval (BRight x) a].
+Lemma setDitv1l a x b :
+  [set` Interval (BSide b x) a] `\ x = [set` Interval (BRight x) a].
 Proof.
+case: b; last by apply: not_setD1; rewrite /= in_itv/= ltxx.
 apply/seteqP; split => [z|z] /=; rewrite !in_itv/=.
   move=> [/andP[xz ->]]; rewrite andbT => /eqP.
   by rewrite lt_neqAle eq_sym => ->.
 move=> /andP[]; rewrite lt_neqAle => /andP[xz zx ->].
 by rewrite andbT; split => //; exact/nesym/eqP.
 Qed.
 
+Lemma setDitv_set2 x y b1 b2 :
+  [set` Interval (BSide b1 x) (BSide b2 y)] `\` [set x; y] = `]x, y[%classic.
+Proof. by rewrite -setDDl setDitv1l setDitv1r. Qed.
+
 End set_itv_porderType.
 Arguments neitv {disp T} _.
 #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `set_itvNyy`")]
@@ -314,6 +334,86 @@ move=> cab; apply/seteqP; split => [x /= [xab /eqP]|x[|]]/=.
   by apply/eqP; rewrite gt_eqF.
 Qed.
 
+Lemma setDitvoo (x y : T) (b1 b2 : bool) :
+  neitv (Interval (BSide b1 x) (BSide b2 y)) ->
+  [set` Interval (BSide b1 x) (BSide b2 y)] `\` `]x, y[ =
+  (if b1 then [set x] else set0) `|` (if b2 then set0 else [set y]).
+Proof.
+move=> /neitv_lt_bnd/= xy.
+apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
+  move: b1 b2 xy.
+  by move=> [] [] /[!bnd_simp]/= + []// -> => ->; rewrite ?(lexx,ltxx,andbF).
+case=> /[swap] /negP; rewrite negb_and.
+move: b1 b2 {xy} => [] [] /= + /andP[]; rewrite ?ltNge !negbK.
+- by move=> /orP[*|->//]; left; exact/le_anti/andP.
+- by case/orP => *; [left|right]; exact/le_anti/andP.
+- by case/orP => ->.
+- by move=> /orP[->//|*]; right; exact/le_anti/andP.
+Qed.
+
+Lemma setDccitv (x y : T) (b1 b2 : bool) :
+  neitv `[x, y] ->
+  `[x, y] `\` [set` Interval (BSide b1 x) (BSide b2 y)] =
+  (if b1 then set0 else [set x]) `|` (if b2 then [set y] else set0).
+Proof.
+move=> /neitv_lt_bnd/= xy.
+apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
+  move: b1 b2 xy.
+  by move=> [] [] /[!bnd_simp]/= + []// -> => ->; rewrite ?(lexx,ltxx,andbF).
+case=> /[swap] /negP; rewrite negb_and.
+move: b1 b2 {xy} => [] [] /= + /andP[]; rewrite -?leNgt.
+- by move=> /orP[/negPf ->//|*]; right; exact/le_anti/andP.
+- by case/orP => /negPf ->.
+- by case/orP => *; [left|right]; exact/le_anti/andP.
+- by move=> /orP[*|/negPf ->//]; left; exact/le_anti/andP.
+Qed.
+
+Lemma setDitvoy a (x : T) (b : bool) :
+  neitv (Interval (BSide b x) a) ->
+  [set` Interval (BSide b x) a] `\` `]x, +oo[ = if b then [set x] else set0.
+Proof.
+move/neitv_lt_bnd => /= bxa; apply/seteqP; split => z/=; rewrite !in_itv/=.
+- case: b {bxa}; rewrite /= andbT; last by case=> /andP[->].
+  by case=> /andP[? _] /negP; rewrite -leNgt => ?; exact/le_anti/andP.
+- case: b bxa => //= /[swap] <-.
+  by move: a => [[] ?|[]]; rewrite !bnd_simp.
+Qed.
+
+Lemma setDitvNyo a (x : T) (b : bool) :
+  neitv (Interval a (BSide b x)) ->
+  [set` Interval a (BSide b x)] `\` `]-oo, x[ = if b then set0 else [set x].
+Proof.
+move/neitv_lt_bnd => /= abx; apply/seteqP; split => z/=; rewrite !in_itv/=.
+- case: b {abx} => /=; first by case=> /andP[_ ->].
+  by case=> /andP[_ ?] /negP; rewrite -leNgt => ?; exact/le_anti/andP.
+- case: b abx => //= /[swap] <-.
+  by move: a => [[] ?|[]]; rewrite !bnd_simp// andbT.
+Qed.
+
+Lemma setD_cbnd_bndy a (x : T) (b : bool) :
+  neitv (Interval (BLeft x) a) ->
+  [set` Interval (BLeft x) a] `\` [set` Interval (BSide b x) +oo%O] =
+  (if b then set0 else [set x]).
+Proof.
+move/neitv_lt_bnd => /= xa; apply/seteqP; split => z/=; rewrite !in_itv/=.
+- case: b {xa}; rewrite /= andbT; first by case=> /andP[->].
+  by case=> /andP[? _] /negP; rewrite -leNgt => ?; exact/le_anti/andP.
+- case: b xa => //= /[swap] <-.
+  by move: a => [[] ?|[]]; rewrite /= !bnd_simp.
+Qed.
+
+Lemma setD_bndc_Nybnd a (x : T) (b : bool) :
+  neitv (Interval a (BRight x)) ->
+  [set` Interval a (BRight x)] `\` [set` Interval -oo%O (BSide b x)] =
+  (if b then [set x] else set0).
+Proof.
+move/neitv_lt_bnd => /= ax; apply/seteqP; split => z/=; rewrite !in_itv/=.
+- case: b {ax} => /=; last by case=> /andP[_ ->].
+  by case=> /andP[_ ?] /negP; rewrite -leNgt => ?; exact/le_anti/andP.
+- case: b ax => //= /[swap] <-.
+  by move: a => [[] ?|[]]; rewrite /= !bnd_simp// andbT.
+Qed.
+
 End set_itv_orderType.
 
 Lemma set_itv_ge disp [T : porderType disp] [b1 b2 : itv_bound T] :

reals/real_interval.v

@@ -56,70 +56,32 @@ Implicit Types x y : R.
 
 Let sup_itv_infty_bnd x b : sup [set` Interval -oo%O (BSide b x)] = x.
 Proof.
-case: b; last first.
-  by rewrite -setUitv1// sup_setU ?sup1// => ? ? ? ->; exact/ltW.
 set s := sup _; apply/eqP; rewrite eq_le; apply/andP; split.
-- apply: ge_sup; last by move=> ? /ltW.
-  by exists (x - 1); rewrite !set_itvE/= ltrBlDr ltrDl.
+- apply: ge_sup; last by move=> ? /lteifW.
+  by exists (x - 1); apply: lteifS; rewrite ltrBlDr ltrDl.
 - rewrite leNgt; apply/negP => sx; pose p := (s + x) / 2.
-  suff /andP[?]: (p < x) && (s < p) by apply/negP; rewrite -leNgt ub_le_sup.
+  suff /andP[?]: (p < x) && (s < p)
+    by apply/negP; rewrite -leNgt ub_le_sup//= in_itv lteifS.
   by rewrite !midf_lt.
 Qed.
 
-Let inf_itv_bnd_infty x b : inf [set` Interval (BSide b x) +oo%O] = x.
-Proof.
-case: b; last by rewrite /inf opp_itv_bndy sup_itv_infty_bnd opprK.
-rewrite -setU1itv// inf_setU ?inf1// => _ b ->.
-by rewrite !set_itvE => /ltW.
-Qed.
-
-Let sup_itv_o_bnd x y b : x < y ->
-  sup [set` Interval (BRight x) (BSide b y)] = y.
-Proof.
-case: b => xy; last first.
-  by rewrite -setUitv1// sup_setU ?sup1// => ? ? /andP[? /ltW ?] ->.
-set B := [set` _]; set A := `]-oo, x]%classic.
-rewrite -(@sup_setU _ A B) //.
-- rewrite -(sup_itv_infty_bnd y true); congr sup.
-  rewrite predeqE => u; split=> [[|/andP[]//]|yu].
-  by rewrite /A !set_itvE => /le_lt_trans; apply.
-  by have [xu|ux] := ltP x u; [right; rewrite /B !set_itvE/= xu| left].
-- by move=> u v; rewrite /A /B => ? /andP[xv _]; rewrite (le_trans _ (ltW xv)).
-Qed.
-
-Let sup_itv_bounded x y a b : (BSide a x < BSide b y)%O ->
-  sup [set` Interval (BSide a x) (BSide b y)] = y.
-Proof.
-case: a => xy; last exact: sup_itv_o_bnd.
-case: b in xy *.
-  by rewrite -setU1itv// sup_setU ?sup_itv_o_bnd// => ? ? -> /andP[/ltW].
-by rewrite -setUitv1// sup_setU ?sup1// => ? ? /andP[_ /ltW ? ->].
-Qed.
-
-Let inf_itv_bnd_o x y b : (BSide b x < BLeft y)%O ->
-  inf [set` Interval (BSide b x) (BLeft y)] = x.
-Proof.
-case: b => xy.
-  by rewrite -setU1itv// inf_setU ?inf1// => _ ? -> /andP[/ltW].
-by rewrite /inf opp_itv_bnd_bnd sup_itv_o_bnd ?opprK // ltrNl opprK.
-Qed.
-
-Let inf_itv_bounded x y a b : (BSide a x < BSide b y)%O ->
-  inf [set` Interval (BSide a x) (BSide b y)] = x.
-Proof.
-case: b => xy; first exact: inf_itv_bnd_o.
-case: a in xy *.
-  by rewrite -setU1itv// inf_setU ?inf1// => ? ? -> /andP[/ltW].
-by rewrite -setUitv1// inf_setU ?inf_itv_bnd_o// => ? ? /andP[? /ltW ?] ->.
-Qed.
-
 Lemma sup_itv a b x : (a < BSide b x)%O ->
   sup [set` Interval a (BSide b x)] = x.
-Proof. by case: a => [b' y|[]]; rewrite ?bnd_simp//= => /sup_itv_bounded->. Qed.
+Proof.
+move=> xy; have /itv_bndbnd_setU : (-oo <= a)%O by rewrite bnd_simp.
+have /[swap]-> := sup_itv_infty_bnd x b; last exact/ltW.
+rewrite sup_setU// => ? ? /= /[!itv_boundlr]/= +/andP[] => /le_trans/[apply].
+by rewrite !bnd_simp => /ltW.
+Qed.
 
 Lemma inf_itv a b x : (BSide b x < a)%O ->
   inf [set` Interval (BSide b x) a] = x.
-Proof. by case: a => [b' y|[]]; rewrite ?bnd_simp//= => /inf_itv_bounded->. Qed.
+Proof.
+case: a => [b' ?|[]]//; rewrite /inf => xa.
+  rewrite opp_itv_bnd_bnd sup_itv// ?opprK//.
+  by move: xa; case: b; case: b'; rewrite !bnd_simp ?lerN2 ?ltrN2.
+by rewrite  ?opp_itv_bndy sup_itv// opprK.
+Qed.
 
 Lemma sup_itvcc x y : x <= y -> sup `[x, y] = y.
 Proof. by move=> *; rewrite sup_itv. Qed.

theories/ftc.v

@@ -1400,10 +1400,7 @@ rewrite integration_by_substitution_decreasing.
     apply/measurable_EFinP.
     by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co.
   rewrite integral_itv_obnd_cbnd//.
-  apply/measurable_EFinP.
-  rewrite -setUitv1; last by rewrite bnd_simp ltrDl.
-  rewrite measurable_funU//; split; last exact: measurable_fun_set1.
-  by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co.
+  by apply/measurable_EFinP; have /measurable_fun_itv_oc := mGFNF' n.
 - by rewrite lerDl.
 - move=> x y /= xaa yaa yx.
   by apply: decrF; rewrite ?in_itv ?andbT/= ?(itvP xaa) ?(itvP yaa).

theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v

@@ -194,10 +194,7 @@ Lemma lebesgue_differentiation_continuous (f : R -> rT^o) (A : set R) (x : R) :
 Proof.
 have ball_itvr r : 0 < r -> `[x - r, x + r] `\` ball x r = [set x + r; x - r].
   move: r => _/posnumP[r].
-  rewrite -setU1itv ?bnd_simp ?lerBlDr -?addrA ?ler_wpDr//.
-  rewrite -setUitv1 ?bnd_simp ?ltrBlDr -?addrA ?ltr_pwDr//.
-  rewrite setUA setUC setUA setDUl !ballE setDv setU0 setDidl// -subset0.
-  by move=> z /= [[]] ->; rewrite in_itv/= ltxx// andbF.
+  by rewrite ballE setDitvoo 1?setUC// neitvE bnd_simp lerD2l// ge0_cp.
 have ball_itv2 r : 0 < r -> ball x r = `[x - r, x + r] `\` [set x + r; x - r].
   move: r => _/posnumP[r].
   rewrite -ball_itvr // setDD setIC; apply/esym/setIidPl.

theories/lebesgue_measure.v

@@ -657,9 +657,8 @@ suff : (lebesgue_measure (`]a - 1, a]%classic%R : set R) =
   rewrite wlength_itv lte_fin ltrBlDr ltrDl ltr01.
   rewrite [in X in X == _]/= EFinN EFinB fin_num_oppeB// addeA subee// add0e.
   by rewrite addeC -sube_eq ?fin_num_adde_defl// subee// => /eqP.
-rewrite -setUitv1// ?bnd_simp; last by rewrite ltrBlDr ltrDl.
-rewrite measureU //; apply/seteqP; split => // x []/=.
-by rewrite in_itv/= => + xa; rewrite xa ltxx andbF.
+rewrite -(setUitv1 true) ?bnd_simp; last by rewrite ltrBlDr ltrDl.
+by rewrite measureU// -(setDitv1r _ a true) setDKI.
 Qed.
 
 Lemma countable_lebesgue_measure0 (A : set R) :
@@ -687,7 +686,7 @@ Let lebesgue_measure_itvoo (a b : R) :
 Proof.
 have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoc a b.
-rewrite 2!wlength_itv => <-; rewrite -setUitv1// measureU//.
+rewrite 2!wlength_itv => <-; rewrite -(setUitv1 true)// measureU//.
 - by have /= -> := lebesgue_measure_set1 b; rewrite adde0.
 - by apply/seteqP; split => // x [/= + xb]; rewrite in_itv/= xb ltxx andbF.
 Qed.
@@ -697,7 +696,7 @@ Let lebesgue_measure_itvcc (a b : R) :
 Proof.
 have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoc a b.
-rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//.
+rewrite 2!wlength_itv => <-; rewrite -(setU1itv false)// measureU//.
 - by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
 - by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
 Qed.
@@ -707,7 +706,7 @@ Let lebesgue_measure_itvco (a b : R) :
 Proof.
 have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoo a b.
-rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//.
+rewrite 2!wlength_itv => <-; rewrite -(setU1itv false)// measureU//.
 - by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
 - by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
 Qed.

theories/lebesgue_stieltjes_measure.v

@@ -576,20 +576,19 @@ have mopoo (x : R) : measurable `]x, +oo[.
 have mnooc (x : R) : measurable `]-oo, x].
   by rewrite -setCitvr; exact/measurableC.
 have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b.
-  case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D.
-  by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF.
+  by rewrite setDitv1r.
 have moo (a b : R) : measurable `]a, b[.
   by rewrite ooE; exact: measurableD.
 have mcc (a b : R) : measurable `[a, b].
   case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
-  by rewrite -setU1itv//; apply/measurableU.
+  by rewrite -(setU1itv false)//; apply/measurableU.
 have mco (a b : R) : measurable `[a, b[.
   case: (boolP (a < b)) => ab; last by rewrite set_itv_ge.
-  by rewrite -setU1itv//; apply/measurableU.
+  by rewrite -(setU1itv false)//; apply/measurableU.
 have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b.
-  by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx.
+  by rewrite setDitv1r.
 case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
-- by rewrite -setU1itv//; exact/measurableU.
+- by rewrite -(setU1itv false)//; exact/measurableU.
 - by rewrite oooE; exact/measurableD.
 - by rewrite set_itvNyy.
 Qed.

theories/measurable_realfun.v

@@ -1399,14 +1399,10 @@ Lemma emeasurable_fun_itv_obnd_cbndP (a : R) (b : itv_bound R) (f : R -> \bar R)
   measurable_fun [set` Interval (BRight a) b] f <->
   measurable_fun [set` Interval (BLeft a) b] f.
 Proof.
-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[].
+have [ab|ba] := leP (BRight a) b; last first.
+  by rewrite !set_itv_ge// -leNgt ?(ltW ba)// -ltBRight_leBLeft.
+rewrite -(setU1itv false)// measurable_funU// (propT (measurable_fun_set1 _)).
+by split => // -[].
 Qed.
 
 Lemma measurable_fun_itv_obnd_cbndP (a : R) (b : itv_bound R) (f : R -> R) :
@@ -1420,12 +1416,10 @@ Lemma emeasurable_fun_itv_bndo_bndcP (a : itv_bound R) (b : R) (f : R -> \bar R)
   measurable_fun [set` Interval a (BLeft b)] f <->
   measurable_fun [set` Interval a (BRight b)] f.
 Proof.
-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[].
+have [ab|ba] := leP a (BLeft b); last first.
+  by rewrite !set_itv_ge// -leNgt// ltW.
+rewrite -(setUitv1 true)// measurable_funU// (propT (measurable_fun_set1 _)).
+by split => // -[].
 Qed.
 
 Lemma measurable_fun_itv_bndo_bndcP (a : itv_bound R) (b : R) (f : R -> R) :