Apply suggestions from code review

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>

4 files changed, 519 insertions, 476 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1e89062..ec479d8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -135,6 +135,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - in `eqtype.v` new lemmas `contra_not_neq`, `contra_eq_not`.
 - in `order.v`, new notations `0^d` and `1^d` for bottom and top elements of
   dual lattices.
+
 - in `interval.v`:
   + Intervals and their bounds of `T` now have canonical ordered type instances
     whose ordering relations are the subset relation and the left to right
@@ -143,8 +144,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
     where the join and meet are intersection and convex hull respectively. If
     `T` is an `orderType`, they are distributive, and the interval bounds are
     totally ordered. (cf Changed section)
-  + New lemmas: `comparable_lteifN`, `itv_total_meet3E`, `itv_total_join3E`,
-    `itv_total_meetsE`, `itv_total_joinsE`
+  + New lemmas: `bound_ltxx`, `subitvE`, `in_itv`, `itv_ge`, `in_itvI`,
+    `itv_total_meet3E`, and `itv_total_join3E`.
+- in `order.v`:
+  + new definition `lteif` and notations `<?<=%O`, `<?<=^d%O`, `_ < _ ?<= if _`,
+    and `_ <^d _ ?<= if _` (cf Changed section).
+  + new lemmas `lteifN`, `comparable_lteifNE`, and
+    `comparable_lteif_(min|max)(l|r)`.
+- in `ssrnum.v`, new lemma `real_lteif_distl`.
 
 - in `matrix.v` new lemma `det_mx11`.
 
@@ -176,51 +183,71 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - in `order.v`, `\join^d_` and `\meet^d_` notations are now properly specialized
   for `dual_display`.
+
 - in `interval.v`:
+  + `x <= y ?< if c` (`lersif`) has been generalized to `porderType`, relocated
+    to `order.v`, and replaced with `x < y ?<= if c'` (`lteif`) where `c'` is
+    negation of `c`.
   + Many definitions and lemmas on intervals such as the membership test are
     generalized from numeric domains to ordered types.
-  + `x <= y ?< if c` (`lersif`) has also been generalized to `porderType` and
-    replaced with `x < y ?<= if c'` (`lteif`) where `c'` is negation of `c`.
-  + Interval bounds `itv_bound : T -> Type` are redefined with two constructors
-    `BRight_if of bool & T` and `BRInfty_if of bool`. `BRight_if true x` and
-    `BRight_if close x` respectively mean open and close bounds as left bounds,
-    and their meanings as right bounds are opposite. `BRInfty_if true` and
-    `BRInfty_if false` respectively means positive and negative infinity. This
-    change gives us the canonical "left to right" ordering of interval bounds.
+  + Interval bounds `itv_bound : Type -> Type` are redefined with two constructors
+    `BSide : bool -> T -> itv_bound T` and `BInfty : bool -> itv_bound T`.
+    New notations `BLeft` and `BRight` are aliases for `BSide true` and `BSide false` respectively.
+    `BInfty false` and `BInfty true` respectively means positive and negative infinity.
+    `BLeft x` and `BRight x` respectively mean close and open bounds as left bounds,
+    and they respectively mean open and close bounds as right bounds.
+    This change gives us the canonical "left to right" ordering of interval bounds.
 
 ### Renamed
 
 - `big_rmcond` -> `big_rmcond_in` (cf Changed section)
 
-- in `interval.v`, we deprecate and rename the following:
-  + `subr_lersif(r0|0r|0)` -> `subr_lteif(r0|0r|0)`
+- in `interval.v`, we deprecate, rename, and relocate to `order.v` the following:
   + `lersif_(trans|anti)` -> `lteif_(trans|anti)`
-  + `lersif(01|xx|NF|S|T|F|W)` -> `lteif(01|xx|NF|S|T|F|W)`
+  + `lersif(xx|NF|S|T|F|W)` -> `lteif(xx|NF|S|T|F|W)`
+  + `lersif_(andb|orb|imply)` -> `lteif_(andb|orb|imply)`
+  + `ltrW_lersif` -> `ltrW_lteif`
+  + `lersifN` -> `lteifNE`
+  + `lersif_(min|max)(l|r)` -> ` lteif_(min|max)(l|r)`
+
+- in `interval.v`, we deprecate, rename, and relocate to `ssrnum.v` the following:
+  + `subr_lersif(r0|0r|0)` -> `subr_lteif(r0|0r|0)`
+  + `lersif01` -> `lteif01`
   + `lersif_(oppl|oppr|0oppr|oppr0|opp2|oppE)` -> `lteif_(oppl|oppr|0oppr|oppr0|opp2|oppE)`
   + `lersif_add2(|l|r)` -> `lteif_add2(|l|r)`
   + `lersif_sub(l|r)_add(l|r)` -> `lteif_sub(l|r)_add(l|r)`
   + `lersif_sub_add(l|r)` -> `lteif_sub_add(l|r)`
-  + `lersif_(andb|orb|imply)` -> `lteif_(andb|orb|imply)`
-  + `ltrW_lersif` -> `ltrW_lteif`
   + `lersif_(p|n)mul2(l|r)` -> `lteif_(p|n)mul2(l|r)`
-  + `real_lersifN` -> `real_lteifN`
+  + `real_lersifN` -> `real_lteifNE`
   + `real_lersif_norm(l|r)` -> `real_lteif_norm(l|r)`
   + `lersif_nnormr` -> `lteif_nnormr`
-  + `lersifN` -> `lteifN`
   + `lersif_norm(l|r)` -> `lteif_norm(l|r)`
   + `lersif_distl` -> `lteif_distl`
-  + `lersif_(min|max)(l|r)` -> ` lteif_(min|max)(l|r)`
   + `lersif_(p|n)div(l|r)_mul(l|r)` -> `lteif_(p|n)div(l|r)_mul(l|r)`
+
+- in `interval.v`, we deprecate and replace the following:
   + `lersif_in_itv` -> `lteif_in_itv`
-  + `itv_intersection` -> `Order.meet`
-  + `itv_intersection1i` -> `meet1x`
-  + `itv_intersectioni1` -> `meetx1`
-  + `itv_intersectionii` -> `meetxx`
-  + `itv_intersectionC` -> `meetC`
-  + `itv_intersectionA` -> `meetA`
+  + `itv_gte` -> `itv_ge`
+  + `l(t|e)r_in_itv` -> `lt_in_itv`
 
 ### Removed
 
+- in `interval.v`, we remove the following:
+  + `le_bound(l|r)` (use `Order.le` instead)
+  + `le_bound(l|r)_refl` (use `lexx` instead)
+  + `le_bound(l|r)_anti` (use `eq_le` instead)
+  + `le_bound(l|r)_trans` (use `le_trans` instead)
+  + `le_bound(l|r)_bb` (use `bound_lexx` instead)
+  + `le_bound(l|r)_total` (use `le_total` instead)
+
+- in `interval.v`, we deprecate the following:
+  + `itv_intersection` (use `Order.meet` instead)
+  + `itv_intersection1i` (use `meet1x` instead)
+  + `itv_intersectioni1` (use `meetx1` instead)
+  + `itv_intersectionii` (use `meetxx` instead)
+  + `itv_intersectionC` (use `meetC` instead)
+  + `itv_intersectionA` (use `meetA` instead)
+
 ### Infrastructure
 
 ### Misc
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 391998a..d6ea076 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -8,12 +8,11 @@ From mathcomp Require Import ssrnum.
 (* This file provide support for intervals in ordered types. The datatype     *)
 (* (interval T) gives a formal characterization of an interval, as the pair   *)
 (* of its right and left bounds.                                              *)
-(*    interval R    == the type of formal intervals on R.                     *)
+(*    interval T    == the type of formal intervals on T.                     *)
 (*    x \in i       == when i is a formal interval on an ordered type,        *)
 (*                     \in can be used to test membership.                    *)
 (*    itvP x_in_i   == where x_in_i has type x \in i, if i is ground,         *)
 (*                     gives a set of rewrite rules that x_in_i imply.        *)
-(* x < y ?<= if c   == x is smaller than y, and strictly if c is false        *)
 (*                                                                            *)
 (* Intervals of T form an partially ordered type (porderType) whose ordering  *)
 (* is the subset relation. If T is a lattice, intervals also form a lattice   *)
@@ -46,101 +45,11 @@ Unset Printing Implicit Defensive.
 Local Open Scope order_scope.
 Import Order.TTheory.
 
-Section LteifPOrder.
-
-Variable (disp : unit) (T : porderType disp).
-Implicit Types (b : bool) (x y z : T).
-
-Definition lteif x y b := if b then x <= y else x < y.
-
-Local Notation "x < y ?<= 'if' b" := (lteif x y b)
-  (at level 70, y at next level,
-  format "x '[hv'  <  y '/'  ?<=  'if'  b ']'") : order_scope.
-
-Lemma lteif_trans x y z b1 b2 :
-  x < y ?<= if b1 -> y < z ?<= if b2 -> x < z ?<= if b1 && b2.
-Proof.
-case: b1 b2 => [][];
-  [exact: le_trans | exact: le_lt_trans | exact: lt_le_trans | exact: lt_trans].
-Qed.
-
-Lemma lteif_anti b1 b2 x y :
-  (x < y ?<= if b1) && (y < x ?<= if b2) = b1 && b2 && (x == y).
-Proof. by case: b1 b2 => [][]; rewrite lte_anti. Qed.
-
-Lemma lteifxx x b : (x < x ?<= if b) = b.
-Proof. by case: b; rewrite /= ltexx. Qed.
-
-Lemma lteifNF x y b : y < x ?<= if ~~ b -> x < y ?<= if b = false.
-Proof. by case: b => [/lt_geF|/le_gtF]. Qed.
-
-Lemma lteifS x y b : x < y -> x < y ?<= if b.
-Proof. by case: b => //= /ltW. Qed.
-
-Lemma lteifT x y : x < y ?<= if true = (x <= y). Proof. by []. Qed.
-
-Lemma lteifF x y : x < y ?<= if false = (x < y). Proof. by []. Qed.
-
-Lemma lteif_orb x y : {morph lteif x y : p q / p || q}.
-Proof. by case=> [][] /=; case: comparableP. Qed.
-
-Lemma lteif_andb x y : {morph lteif x y : p q / p && q}.
-Proof. by case=> [][] /=; case: comparableP. Qed.
-
-Lemma lteif_imply b1 b2 x y : b1 ==> b2 -> x < y ?<= if b1 -> x < y ?<= if b2.
-Proof. by case: b1 b2 => [][] //= _ /ltW. Qed.
-
-Lemma lteifW b x y : x < y ?<= if b -> x <= y.
-Proof. by case: b => // /ltW. Qed.
-
-Lemma ltrW_lteif b x y : x < y -> x < y ?<= if b.
-Proof. by case: b => // /ltW. Qed.
-
-Lemma comparable_lteifN x y b :
-  x >=< y -> x < y ?<= if ~~b = ~~ (y < x ?<= if b).
-Proof. by case: b => /=; case: comparableP. Qed.
-
-End LteifPOrder.
-
-Notation "x < y ?<= 'if' b" := (lteif x y b)
-  (at level 70, y at next level,
-  format "x '[hv'  <  y '/'  ?<=  'if'  b ']'") : order_scope.
-
-Notation "x < y ?<= 'if' b" := (@lteif ring_display _ x y b)
-  (at level 70, y at next level,
-  format "x '[hv'  <  y '/'  ?<=  'if'  b ']'") : ring_scope.
-
-Section LteifTotal.
-
-Variable (disp : unit) (T : orderType disp) (b : bool) (x y z e : T).
-
-Lemma lteif_minr :
-  (x < Order.min y z ?<= if b) = (x < y ?<= if b) && (x < z ?<= if b).
-Proof. by case: b; rewrite /= (le_minr, lt_minr). Qed.
-
-Lemma lteif_minl :
-  (Order.min y z < x ?<= if b) = (y < x ?<= if b) || (z < x ?<= if b).
-Proof. by case: b; rewrite /= (le_minl, lt_minl). Qed.
-
-Lemma lteif_maxr :
-  (x < Order.max y z ?<= if b) = (x < y ?<= if b) || (x < z ?<= if b).
-Proof. by case: b; rewrite /= (le_maxr, lt_maxr). Qed.
-
-Lemma lteif_maxl :
-  (Order.max y z < x ?<= if b) = (y < x ?<= if b) && (z < x ?<= if b).
-Proof. by case: b; rewrite /= (le_maxl, lt_maxl). Qed.
-
-Lemma lteifN : (x < y ?<= if ~~ b) = ~~ (y < x ?<= if b).
-Proof. by rewrite comparable_lteifN ?comparableT. Qed.
-
-End LteifTotal.
-
-Variant itv_bound (T : Type) : Type :=
-  BRight_if of bool & T | BRInfty_if of bool.
-Notation BLeft := (BRight_if false).
-Notation BRight := (BRight_if true).
-Notation "'-oo'" := (BRInfty_if _ false) (at level 0) : order_scope.
-Notation "'+oo'" := (BRInfty_if _ true) (at level 0) : order_scope.
+Variant itv_bound (T : Type) : Type := BSide of bool & T | BInfty of bool.
+Notation BLeft := (BSide true).
+Notation BRight := (BSide false).
+Notation "'-oo'" := (BInfty _ true) (at level 0) : order_scope.
+Notation "'+oo'" := (BInfty _ false) (at level 0) : order_scope.
 Variant interval (T : Type) := Interval of itv_bound T & itv_bound T.
 
 (* We provide the 9 following notations to help writing formal intervals *)
@@ -191,8 +100,8 @@ Variable T : eqType.
 
 Definition eq_itv_bound (b1 b2 : itv_bound T) : bool :=
   match b1, b2 with
-    | BRight_if a x, BRight_if b y => (a == b) && (x == y)
-    | BRInfty_if a, BRInfty_if b => a == b
+    | BSide a x, BSide b y => (a == b) && (x == y)
+    | BInfty a, BInfty b => a == b
     | _, _ => false
   end.
 
@@ -229,9 +138,9 @@ Variable T : choiceType.
 
 Lemma itv_bound_can :
   cancel (fun b : itv_bound T =>
-            match b with BRight_if b x => (b, Some x) | BRInfty_if b => (b, None) end)
+            match b with BSide b x => (b, Some x) | BInfty b => (b, None) end)
          (fun b =>
-            match b with (b, Some x) => BRight_if b x | (b, None) => BRInfty_if _ b end).
+            match b with (b, Some x) => BSide b x | (b, None) => BInfty _ b end).
 Proof. by case. Qed.
 
 Lemma interval_can :
@@ -266,19 +175,19 @@ Export IntervalChoice.Exports.
 Section IntervalPOrder.
 
 Variable (disp : unit) (T : porderType disp).
-Implicit Types (x y z : T) (i : interval T).
+Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T).
 
-Definition le_bound (b1 b2 : itv_bound T) :=
+Definition le_bound b1 b2 :=
   match b1, b2 with
     | -oo, _ | _, +oo => true
-    | BRight_if b1 x1, BRight_if b2 x2 => x1 < x2 ?<= if b1 ==> b2
+    | BSide b1 x1, BSide b2 x2 => x1 < x2 ?<= if b2 ==> b1
     | _, _ => false
   end.
 
-Definition lt_bound (b1 b2 : itv_bound T) :=
+Definition lt_bound b1 b2 :=
   match b1, b2 with
-    | -oo, +oo | -oo, BRight_if _ _ | BRight_if _ _, +oo => true
-    | BRight_if b1 x1, BRight_if b2 x2 => x1 < x2 ?<= if ~~ b1 && b2
+    | -oo, +oo | -oo, BSide _ _ | BSide _ _, +oo => true
+    | BSide b1 x1, BSide b2 x2 => x1 < x2 ?<= if b1 && ~~ b2
     | _, _ => false
   end.
 
@@ -302,13 +211,15 @@ Definition itv_bound_porderMixin :=
 Canonical itv_bound_porderType :=
   POrderType (itv_bound_display disp) (itv_bound T) itv_bound_porderMixin.
 
-Lemma le_bound_bb x b1 b2 : (BRight_if b1 x <= BRight_if b2 x) = (b1 ==> b2).
+Lemma bound_lexx c1 c2 x : (BSide c1 x <= BSide c2 x) = (c2 ==> c1).
 Proof. by rewrite /<=%O /= lteifxx. Qed.
 
+Lemma bound_ltxx c1 c2 x : (BSide c1 x < BSide c2 x) = (c1 && ~~ c2).
+Proof. by rewrite /<%O /= lteifxx. Qed.
+
 Definition subitv i1 i2 :=
-  match i1, i2 with
-    | Interval a1 b1, Interval a2 b2 => (a2 <= a1) && (b1 <= b2)
-  end.
+  let: Interval b1l b1r := i1 in
+  let: Interval b2l b2r := i2 in (b2l <= b1l) && (b1r <= b2r).
 
 Lemma subitv_refl : reflexive subitv.
 Proof. by case=> /= ? ?; rewrite !lexx. Qed.
@@ -333,43 +244,74 @@ Definition pred_of_itv i : pred T := [pred x | `[x, x] <= i].
 
 Canonical Structure itvPredType := PredType pred_of_itv.
 
+Lemma subitvE b1l b1r b2l b2r :
+  (Interval b1l b1r <= Interval b2l b2r) = (b2l <= b1l) && (b1r <= b2r).
+Proof. by []. Qed.
+
+Lemma in_itv x i :
+  x \in i =
+  let: Interval l u := i in
+  match l with
+    | BSide b lb => lb < x ?<= if b
+    | BInfty b => b
+  end &&
+  match u with
+    | BSide b ub => x < ub ?<= if ~~ b
+    | BInfty b => ~~ b
+  end.
+Proof. by case: i => [[? ?|[]][|[]]]. Qed.
+
 Lemma itv_boundlr bl br x :
   (x \in Interval bl br) = (bl <= BLeft x) && (BRight x <= br).
 Proof. by []. Qed.
 
+Lemma itv_splitI bl br x :
+  x \in Interval bl br = (x \in Interval bl +oo) && (x \in Interval -oo br).
+Proof. by rewrite !itv_boundlr andbT. Qed.
+
 Lemma subitvP i1 i2 : i1 <= i2 -> {subset i1 <= i2}.
-Proof.
-by case: i1 i2 => [[b2 l2|[]][b2' u2|[]]][[b1 l1|[]][b1' u1|[]]]
-          /andP [] /= ha hb x /andP [ha' hb']; apply/andP; split => //;
-  (apply/lteif_imply: (lteif_trans ha ha'); case: b1 b2 ha ha' => [][]) ||
-  (apply/lteif_imply: (lteif_trans hb' hb); case: b1' b2' hb hb' => [][]).
-Qed.
+Proof. by move=> ? ? /le_trans; exact. Qed.
+
+Lemma subitvPl b1l b2l br :
+  b2l <= b1l -> {subset Interval b1l br <= Interval b2l br}.
+Proof. by move=> ?; apply: subitvP; rewrite subitvE lexx andbT. Qed.
 
-Lemma subitvEl (a1 a2 b : itv_bound T) :
-  (Interval a1 b <= Interval a2 b) = (a2 <= a1).
-Proof. by rewrite [LHS]/<=%O /= lexx andbT. Qed.
+Lemma subitvPr bl b1r b2r :
+  b1r <= b2r -> {subset Interval bl b1r <= Interval bl b2r}.
+Proof. by move=> ?; apply: subitvP; rewrite subitvE lexx. Qed.
 
-Lemma subitvEr (a b1 b2 : itv_bound T) :
-  (Interval a b1 <= Interval a b2) = (b1 <= b2).
-Proof. by rewrite [LHS]/<=%O /= lexx. Qed.
+Lemma itv_xx x cl cr y :
+  y \in Interval (BSide cl x) (BSide cr x) = cl && ~~ cr && (y == x).
+Proof. by case: cl cr => [] []; rewrite [LHS]lteif_anti // eq_sym. Qed.
 
-Lemma subitvPl (a1 a2 b : itv_bound T) :
-  a2 <= a1 -> {subset Interval a1 b <= Interval a2 b}.
-Proof. by move=> lea; apply: subitvP; rewrite subitvEl. Qed.
+Lemma boundl_in_itv c x b : x \in Interval (BSide c x) b = c && (BRight x <= b).
+Proof. by rewrite itv_boundlr bound_lexx. Qed.
+
+Lemma boundr_in_itv c x b :
+  x \in Interval b (BSide c x) = ~~ c && (b <= BLeft x).
+Proof. by rewrite itv_boundlr bound_lexx implybF andbC. Qed.
+
+Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
 
-Lemma subitvPr (a b1 b2 : itv_bound T) :
-  b1 <= b2 -> {subset Interval a b1 <= Interval a b2}.
-Proof. by move=> leb; apply: subitvP; rewrite subitvEr. Qed.
+Lemma lt_in_itv bl br x : x \in Interval bl br -> bl < br.
+Proof. by case/andP; apply/le_lt_trans. Qed.
+
+Lemma lteif_in_itv cl cr yl yr x :
+  x \in Interval (BSide cl yl) (BSide cr yr) -> yl < yr ?<= if cl && ~~ cr.
+Proof. exact: lt_in_itv. Qed.
+
+Lemma itv_ge b1 b2 : ~~ (b1 < b2) -> Interval b1 b2 =i pred0.
+Proof. by move=> ltb12 y; apply/contraNF: ltb12; apply/lt_in_itv. Qed.
 
 Definition itv_decompose i x : Prop :=
   let: Interval l u := i in
   (match l return Prop with
-     | BRight_if b lb => lb < x ?<= if ~~ b
-     | BRInfty_if b => ~~ b
+     | BSide b lb => lb < x ?<= if b
+     | BInfty b => b
    end *
    match u return Prop with
-     | BRight_if b ub => x < ub ?<= if b
-     | BRInfty_if b => b
+     | BSide b ub => x < ub ?<= if ~~ b
+     | BInfty b => ~~ b
    end)%type.
 
 Lemma itv_dec : forall x i, reflect (itv_decompose i x) (x \in i).
@@ -377,36 +319,6 @@ Proof. by move=> ? [[? ?|[]][? ?|[]]]; apply: (iffP andP); case. Qed.
 
 Arguments itv_dec {x i}.
 
-Lemma itv_xx x bl br :
-  Interval (BRight_if bl x) (BRight_if br x) =i
-  if ~~ bl && br then pred1 x else pred0.
-Proof.
-by move=> y; rewrite itv_boundlr lteif_anti implybF eq_sym; case: (~~ _ && _).
-Qed.
-
-Lemma itv_gte ba xa bb xb :
-  xb < xa ?<= if ba || ~~ bb ->
-  Interval (BRight_if ba xa) (BRight_if bb xb) =i pred0.
-Proof.
-move=> ? y; apply/negP; rewrite inE /= itv_boundlr.
-case/andP => lexay /(lteif_trans lexay).
-by rewrite implybF lteifNF //= negb_and negbK.
-Qed.
-
-Lemma boundl_in_itv : forall ba xa b,
-  xa \in Interval (BRight_if ba xa) b =
-  if ba then false else BRight xa <= b.
-Proof. by case=> xa [b xb|[]]; rewrite itv_boundlr /<=%O /= ?(lexx, ltxx). Qed.
-
-Lemma boundr_in_itv : forall bb xb a,
-  xb \in Interval a (BRight_if bb xb) =
-  if bb then a <= BLeft xb else false.
-Proof.
-by case=> xb [b xa|[]]; rewrite itv_boundlr andbC /<=%O /= ?(lexx, ltxx).
-Qed.
-
-Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
-
 (* we compute a set of rewrite rules associated to an interval *)
 Definition itv_rewrite i x : Type :=
   let: Interval l u := i in
@@ -414,13 +326,13 @@ Definition itv_rewrite i x : Type :=
        | BLeft a => (a <= x) * (x < a = false)
        | BRight a => (a <= x) * (a < x) * (x <= a = false) * (x < a = false)
        | -oo => forall x : T, x == x
-       | +oo => forall x : T, x == x (* ? *)
+       | +oo => forall b : bool, unkeyed b = false
      end *
      match u with
        | BRight b => (x <= b) * (b < x = false)
        | BLeft b => (x <= b) * (x < b) * (b <= x = false) * (b < x = false)
        | +oo => forall x : T, x == x
-       | -oo => forall x : T, x == x (* ? *)
+       | -oo => forall b : bool, unkeyed b = false
      end *
      match l, u with
        | BLeft a, BRight b =>
@@ -437,29 +349,15 @@ Definition itv_rewrite i x : Type :=
        | _, _ => forall x : T, x == x
      end)%type.
 
-Lemma itvP : forall x i, x \in i -> itv_rewrite i x.
+Lemma itvP x i : x \in i -> itv_rewrite i x.
 Proof.
-move=> x [[[]a|[]][[]b|[]]] /andP [] ha hb; do !split;
-  rewrite ?bound_in_itv //=; do 1?[apply/negbTE; rewrite (le_gtF, lt_geF)];
-  try by [| apply: ltW | move: (lteif_trans ha hb) => //=; exact: ltW].
+case: i => [[[]a|[]][[]b|[]]] /andP [] ha hb; rewrite /= ?bound_in_itv;
+  do ![split | apply/negbTE; rewrite (le_gtF, lt_geF)];
+  by [|apply: ltW | move: (lteif_trans ha hb) => //=; exact: ltW].
 Qed.
 
 Arguments itvP [x i].
 
-Lemma lteif_in_itv ba bb xa xb x :
-  x \in Interval (BRight_if ba xa) (BRight_if bb xb) ->
-  xa < xb ?<= if ~~ ba && bb.
-Proof. by case: ba bb => [][] /itvP /= ->. Qed.
-
-Lemma ltr_in_itv ba bb xa xb x :
-  ba || ~~ bb -> x \in Interval (BRight_if ba xa) (BRight_if bb xb) ->
-  xa < xb.
-Proof. by case: ba bb => [][] // _ /itvP ->. Qed.
-
-Lemma ler_in_itv ba bb xa xb x :
-  x \in Interval (BRight_if ba xa) (BRight_if bb xb) -> xa <= xb.
-Proof. by move/lteif_in_itv/lteifW. Qed.
-
 End IntervalPOrder.
 
 Section IntervalLattice.
@@ -471,60 +369,58 @@ Definition bound_meet bl br : itv_bound T :=
   match bl, br with
     | -oo, _ | _, -oo => -oo
     | +oo, b | b, +oo => b
-    | BRight_if xb x, BRight_if yb y =>
-      BRight_if ((~~ (x <= y) || xb) && (~~ (y <= x) || yb)) (x `&` y)
+    | BSide xb x, BSide yb y =>
+      BSide (((x <= y) && xb) || ((y <= x) && yb)) (x `&` y)
   end.
 
 Definition bound_join bl br : itv_bound T :=
   match bl, br with
     | -oo, b | b, -oo => b
     | +oo, _ | _, +oo => +oo
-    | BRight_if xb x, BRight_if yb y =>
-      BRight_if ((x <= y) && yb || (y <= x) && xb) (x `|` y)
+    | BSide xb x, BSide yb y =>
+      BSide ((~~ (x <= y) || yb) && (~~ (y <= x) || xb)) (x `|` y)
   end.
 
 Lemma bound_meetC : commutative bound_meet.
 Proof.
-case=> [? ?|[]][? ?|[]] //=; rewrite meetC; congr BRight_if.
-by case: lcomparableP; rewrite ?andbT // andbC.
+case=> [? ?|[]][? ?|[]] //=; rewrite meetC; congr BSide.
+by case: lcomparableP; rewrite ?orbF // orbC.
 Qed.
 
 Lemma bound_joinC : commutative bound_join.
 Proof.
-case=> [? ?|[]][? ?|[]] //=; rewrite joinC; congr BRight_if.
-by case: lcomparableP; rewrite ?orbF // orbC.
+case=> [? ?|[]][? ?|[]] //=; rewrite joinC; congr BSide.
+by case: lcomparableP; rewrite ?andbT // andbC.
 Qed.
 
 Lemma bound_meetA : associative bound_meet.
 Proof.
-case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !lexI meetA; congr BRight_if.
+case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !lexI meetA; congr BSide.
 by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->];
-  case: (lcomparableP x z) => [|||//<-] //=;
-  case: (lcomparableP x y) => //=; case: (lcomparableP y z);
-  rewrite //= ?orbT ?andbT ?lexx ?andbA.
+  case: (lcomparableP x z) => [|||//<-]; case: (lcomparableP x y);
+  rewrite //= ?andbF ?orbF ?lexx ?orbA //; case: (lcomparableP y z).
 Qed.
 
 Lemma bound_joinA : associative bound_join.
 Proof.
-case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !leUx joinA //.
+case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !leUx joinA; congr BSide.
 by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->];
-  case: (lcomparableP x z) => [|||//<-] //=;
-  case: (lcomparableP x y) => //=; case: (lcomparableP y z);
-  rewrite //= ?andbF ?orbF ?lexx ?orbA.
+  case: (lcomparableP x z) => [|||//<-]; case: (lcomparableP x y);
+  rewrite //= ?orbT ?andbT ?lexx ?andbA //; case: (lcomparableP y z).
 Qed.
 
 Lemma bound_meetKU b2 b1 : bound_join b1 (bound_meet b1 b2) = b1.
 Proof.
-case: b1 b2 => [? ?|[]][? ?|[]] //=; congr BRight_if;
-  rewrite ?meetKU ?joinxx ?leIl ?lexI ?lexx ?orbb //=.
-by case: lcomparableP; rewrite ?andbT /= ?orbb ?andbK.
+case: b1 b2 => [? ?|[]][? ?|[]] //=;
+  rewrite ?meetKU ?joinxx ?leIl ?lexI ?lexx ?andbb //=; congr BSide.
+by case: lcomparableP; rewrite ?orbF /= ?andbb ?orbK.
 Qed.
 
 Lemma bound_joinKI b2 b1 : bound_meet b1 (bound_join b1 b2) = b1.
 Proof.
-case: b1 b2 => [? ?|[]][? ?|[]] //=; congr BRight_if;
-  rewrite ?joinKI ?meetxx ?leUl ?leUx ?lexx ?andbb //=.
-by case: lcomparableP; rewrite ?andbT ?andbb ?orKb.
+case: b1 b2 => [? ?|[]][? ?|[]] //=;
+  rewrite ?joinKI ?meetxx ?leUl ?leUx ?lexx ?orbb //=; congr BSide.
+by case: lcomparableP; rewrite ?orbF ?orbb ?andKb.
 Qed.
 
 Lemma bound_leEmeet b1 b2 : (b1 <= b2) = (bound_meet b1 b2 == b1).
@@ -594,7 +490,7 @@ Canonical interval_bLatticeType :=
 Canonical interval_tbLatticeType :=
   TBLatticeType (interval T) (TopMixin itv_lex1).
 
-Lemma in_itv_meet x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2).
+Lemma in_itvI x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2).
 Proof. exact: lexI. Qed.
 
 End IntervalLattice.
@@ -623,97 +519,60 @@ Canonical interval_distrLatticeType :=
 Canonical interval_bDistrLatticeType := [bDistrLatticeType of interval T].
 Canonical interval_tbDistrLatticeType := [tbDistrLatticeType of interval T].
 
-Lemma itv_splitU (xc : T) bc a b : xc \in Interval a b ->
-  forall y, y \in Interval a b =
-    (y \in Interval a (BRight_if bc xc)) ||
-    (y \in Interval (BRight_if bc xc) b).
+Lemma itv_splitU c a b : a <= c <= b ->
+  forall y, y \in Interval a b = (y \in Interval a c) || (y \in Interval c b).
 Proof.
-move=> xc_in y; move: xc_in.
-rewrite !itv_boundlr ![BRight_if _ _ <= BRight_if _ _]/<=%O /= lteifN.
-case/andP => leaxc lexcb; case: (leP a) => leay; case: (leP _ b) => leyb;
-  rewrite ?andbT ?andbF ?orbF ?orbN //=; [apply/esym/negbTE | apply/esym/negbF].
-- by rewrite -lteifN; apply/lteif_imply: (le_lt_trans lexcb leyb).
-- by apply/lteif_imply: (lt_le_trans leay leaxc).
+case/andP => leac lecb y.
+rewrite !itv_boundlr !(ltNge (BLeft y) _ : (BRight y <= _) = _).
+case: (leP a) (leP b) (leP c) => leay [] leby [] lecy //=.
+- by case: leP lecy (le_trans lecb leby).
+- by case: leP leay (le_trans leac lecy).
 Qed.
 
-Lemma itv_splitU2 x a b : x \in Interval a b ->
+Lemma itv_splitUeq x a b : x \in Interval a b ->
   forall y, y \in Interval a b =
-    [|| (y \in Interval a (BLeft x)), (y == x)
-      | (y \in Interval (BRight x) b)].
+    [|| y \in Interval a (BLeft x), y == x | y \in Interval (BRight x) b].
 Proof.
-move=> xab y; rewrite (itv_splitU false xab y); congr (_ || _).
-rewrite (@itv_splitU x true _ _ _ y); first by rewrite itv_xx inE.
-by move: xab; rewrite boundl_in_itv itv_boundlr => /andP [].
+case/andP => ax xb y; rewrite (@itv_splitU (BLeft x)) ?ax ?ltW //.
+by congr orb; rewrite (@itv_splitU (BRight x)) ?bound_lexx // itv_xx.
 Qed.
 
 Lemma itv_total_meet3E i1 i2 i3 :
   i1 `&` i2 `&` i3 \in [:: i1 `&` i2; i1 `&` i3; i2 `&` i3].
 Proof.
-rewrite !inE /eq_op; case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r] /=.
-case: (leP b2l b1l); case: (leP b3l b2l); case: (leP b3l b1l);
-  case: (leP b1r b2r); case: (leP b2r b3r); case: (leP b1r b3r);
-  rewrite ?eqxx ?andbT ?orbT //= => b13r b23r b12r b31l b32l b21l.
-- by case: leP b13r (lt_trans b23r b12r).
-- by case: leP b31l (le_trans b32l b21l).
-- by case: leP b31l (le_trans b32l b21l).
-- by case: leP b31l (le_trans b32l b21l).
-- by case: leP b13r (lt_trans b23r b12r).
+case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r]; rewrite !inE /eq_op /=.
+case: (leP b1l b2l); case: (leP b1l b3l); case: (leP b2l b3l);
+  case: (leP b1r b2r); case: (leP b1r b3r); case: (leP b2r b3r);
+  rewrite ?eqxx ?orbT //= => b23r b13r b12r b23l b13l b12l.
+- by case: leP b13r (le_trans b12r b23r).
+- by case: leP b13l (le_trans b12l b23l).
+- by case: leP b13l (le_trans b12l b23l).
 - by case: leP b13r (le_trans b12r b23r).
 - by case: leP b13r (le_trans b12r b23r).
-- by case: leP b31l (lt_trans b21l b32l).
-- by case: leP b31l (lt_trans b21l b32l).
-- by case: leP b31l (lt_trans b21l b32l).
+- by case: leP b13l (lt_trans b23l b12l).
+- by case: leP b13r (lt_trans b23r b12r).
+- by case: leP b13l (lt_trans b23l b12l).
+- by case: leP b13r (lt_trans b23r b12r).
+- by case: leP b13r (lt_trans b23r b12r).
 Qed.
 
 Lemma itv_total_join3E i1 i2 i3 :
   i1 `|` i2 `|` i3 \in [:: i1 `|` i2; i1 `|` i3; i2 `|` i3].
 Proof.
-rewrite !inE /eq_op; case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r] /=.
-case: (leP b2l b1l); case: (leP b3l b2l); case: (leP b3l b1l);
-  case: (leP b1r b2r); case: (leP b2r b3r); case: (leP b1r b3r);
-  rewrite ?eqxx ?andbT ?orbT //= => b13r b23r b12r b31l b32l b21l.
-- by case: leP b31l (le_trans b32l b21l).
-- by case: leP b31l (le_trans b32l b21l).
-- by case: leP b31l (le_trans b32l b21l).
-- by case: leP b13r (lt_trans b23r b12r).
-- by case: leP b13r (lt_trans b23r b12r).
-- by case: leP b13r (le_trans b12r b23r).
+case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r]; rewrite !inE /eq_op /=.
+case: (leP b1l b2l); case: (leP b1l b3l); case: (leP b2l b3l);
+  case: (leP b1r b2r); case: (leP b1r b3r); case: (leP b2r b3r);
+  rewrite ?eqxx ?orbT //= => b23r b13r b12r b23l b13l b12l.
 - by case: leP b13r (le_trans b12r b23r).
-- by case: leP b31l (lt_trans b21l b32l).
-- by case: leP b31l (lt_trans b21l b32l).
 - by case: leP b13r (le_trans b12r b23r).
-Qed.
-
-Lemma itv_total_meetsE (S : Type) (s : seq S) (f : S -> interval T) :
-  \meet_(ix <- s) f ix \in
-  `]-oo, +oo[ :: [seq f ix `&` f ix' | ix <- s, ix' <- s].
-Proof.
-case: s => [|x s]; rewrite ?big_nil // inE; apply/orP; right.
-elim: s x => [|y s ih] x; rewrite !big_cons;
-  first by rewrite big_nil meetx1 inE meetxx.
-move: (itv_total_meet3E (f x) (f y) (\meet_(ix <- s) f ix)).
-rewrite meetA 3!inE => /or3P [] /eqP ->.
-- by rewrite /= !inE eqxx orbT.
-- move: (ih x); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=.
-  by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT.
-- move: (ih y); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=.
-  by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT.
-Qed.
-
-Lemma itv_total_joinsE (S : Type) (s : seq S) (f : S -> interval T) :
-  \join_(ix <- s) f ix \in
-  Interval +oo -oo :: [seq f ix `|` f ix' | ix <- s, ix' <- s].
-Proof.
-case: s => [|x s]; rewrite ?big_nil // inE; apply/orP; right.
-elim: s x => [|y s ih] x; rewrite !big_cons;
-  first by rewrite big_nil joinx0 inE joinxx.
-move: (itv_total_join3E (f x) (f y) (\join_(ix <- s) f ix)).
-rewrite joinA 3!inE => /or3P [] /eqP ->.
-- by rewrite /= !inE eqxx orbT.
-- move: (ih x); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=.
-  by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT.
-- move: (ih y); rewrite big_cons 2!allpairs_consr 2!mem_cat allpairs_consr /=.
-  by rewrite !(mem_cat, inE) -!orbA => /or4P [] ->; rewrite ?orbT.
+- by case: leP b13l (le_trans b12l b23l).
+- by case: leP b13l (le_trans b12l b23l).
+- by case: leP b13l (le_trans b12l b23l).
+- by case: leP b13r (lt_trans b23r b12r).
+- by case: leP b13l (lt_trans b23l b12l).
+- by case: leP b13l (lt_trans b23l b12l).
+- by case: leP b13l (lt_trans b23l b12l).
+- by case: leP b13r (lt_trans b23r b12r).
 Qed.
 
 End IntervalTotal.
@@ -721,178 +580,34 @@ End IntervalTotal.
 Local Open Scope ring_scope.
 Import GRing.Theory Num.Theory.
 
-Section LteifNumDomain.
-
-Variable R : numDomainType.
-Implicit Types (b : bool) (x y z : R).
-
-Local Notation "x < y ?<= 'if' b" := (@lteif _ R x y b)
-  (at level 70, y at next level,
-  format "x '[hv'  <  y '/'  ?<=  'if'  b ']'") : ring_scope.
-
-Lemma subr_lteifr0 b (x y : R) : (y - x < 0 ?<= if b) = (y < x ?<= if b).
-Proof. by case: b => /=; rewrite subr_lte0. Qed.
-
-Lemma subr_lteif0r b (x y : R) : (0 < y - x ?<= if b) = (x < y ?<= if b).
-Proof. by case: b => /=; rewrite subr_gte0. Qed.
-
-Definition subr_lteif0 := (subr_lteifr0, subr_lteif0r).
-
-Lemma lteif01 b : 0 < 1 ?<= if b.
-Proof. by case: b; rewrite /= lter01. Qed.
-
-Lemma lteif_oppl b x y : - x < y ?<= if b = (- y < x ?<= if b).
-Proof. by case: b; rewrite /= lter_oppl. Qed.
-
-Lemma lteif_oppr b x y : x < - y ?<= if b = (y < - x ?<= if b).
-Proof. by case: b; rewrite /= lter_oppr. Qed.
-
-Lemma lteif_0oppr b x : 0 < - x ?<= if b = (x < 0 ?<= if b).
-Proof. by case: b; rewrite /= (oppr_ge0, oppr_gt0). Qed.
-
-Lemma lteif_oppr0 b x : - x < 0 ?<= if b = (0 < x ?<= if b).
-Proof. by case: b; rewrite /= (oppr_le0, oppr_lt0). Qed.
-
-Lemma lteif_opp2 b : {mono -%R : x y /~ x < y ?<= if b}.
-Proof. by case: b => ? ?; rewrite /= lter_opp2. Qed.
-
-Definition lteif_oppE := (lteif_0oppr, lteif_oppr0, lteif_opp2).
-
-Lemma lteif_add2l b x : {mono +%R x : y z / y < z ?<= if b}.
-Proof. by case: b => ? ?; rewrite /= lter_add2. Qed.
-
-Lemma lteif_add2r b x : {mono +%R^~ x : y z / y < z ?<= if b}.
-Proof. by case: b => ? ?; rewrite /= lter_add2. Qed.
-
-Definition lteif_add2 := (lteif_add2l, lteif_add2r).
-
-Lemma lteif_subl_addr b x y z : (x - y < z ?<= if b) = (x < z + y ?<= if b).
-Proof. by case: b; rewrite /= lter_sub_addr. Qed.
-
-Lemma lteif_subr_addr b x y z : (x < y - z ?<= if b) = (x + z < y ?<= if b).
-Proof. by case: b; rewrite /= lter_sub_addr. Qed.
-
-Definition lteif_sub_addr := (lteif_subl_addr, lteif_subr_addr).
-
-Lemma lteif_subl_addl b x y z : (x - y < z ?<= if b) = (x < y + z ?<= if b).
-Proof. by case: b; rewrite /= lter_sub_addl. Qed.
-
-Lemma lteif_subr_addl b x y z : (x < y - z ?<= if b) = (z + x < y ?<= if b).
-Proof. by case: b; rewrite /= lter_sub_addl. Qed.
-
-Definition lteif_sub_addl := (lteif_subl_addl, lteif_subr_addl).
-
-Lemma lteif_pmul2l b x : 0 < x -> {mono *%R x : y z / y < z ?<= if b}.
-Proof. by case: b => ? ? ?; rewrite /= lter_pmul2l. Qed.
-
-Lemma lteif_pmul2r b x : 0 < x -> {mono *%R^~ x : y z / y < z ?<= if b}.
-Proof. by case: b => ? ? ?; rewrite /= lter_pmul2r. Qed.
-
-Lemma lteif_nmul2l b x : x < 0 -> {mono *%R x : y z /~ y < z ?<= if b}.
-Proof. by case: b => ? ? ?; rewrite /= lter_nmul2l. Qed.
-
-Lemma lteif_nmul2r b x : x < 0 -> {mono *%R^~ x : y z /~ y < z ?<= if b}.
-Proof. by case: b => ? ? ?; rewrite /= lter_nmul2r. Qed.
-
-Lemma real_lteifN x y b : x \is Num.real -> y \is Num.real ->
-  x < y ?<= if ~~b = ~~ (y < x ?<= if b).
-Proof. by move=> ? ?; rewrite comparable_lteifN ?real_comparable. Qed.
-
-Lemma real_lteif_norml b x y :
-  x \is Num.real ->
-  (`|x| < y ?<= if b) = ((- y < x ?<= if b) && (x < y ?<= if b)).
-Proof. by case: b => ?; rewrite /= real_lter_norml. Qed.
-
-Lemma real_lteif_normr b x y :
-  y \is Num.real ->
-  (x < `|y| ?<= if b) = ((x < y ?<= if b) || (x < - y ?<= if b)).
-Proof. by case: b => ?; rewrite /= real_lter_normr. Qed.
-
-Lemma lteif_nnormr b x y : y < 0 ?<= if ~~ b -> (`|x| < y ?<= if b) = false.
-Proof. by case: b => ?; rewrite /= lter_nnormr. Qed.
-
-End LteifNumDomain.
-
-Section LteifRealDomain.
-
-Variable (R : realDomainType) (b : bool) (x y z e : R).
-
-Lemma lteif_norml :
-  (`|x| < y ?<= if b) = (- y < x ?<= if b) && (x < y ?<= if b).
-Proof. by case: b; rewrite /= lter_norml. Qed.
-
-Lemma lteif_normr :
-  (x < `|y| ?<= if b) = (x < y ?<= if b) || (x < - y ?<= if b).
-Proof. by case: b; rewrite /= lter_normr. Qed.
-
-Lemma lteif_distl :
-  (`|x - y| < e ?<= if b) = (y - e < x ?<= if b) && (x < y + e ?<= if b).
-Proof. by case: b; rewrite /= lter_distl. Qed.
-
-End LteifRealDomain.
-
-Section LteifField.
-
-Variable (F : numFieldType) (b : bool) (z x y : F).
-
-Lemma lteif_pdivl_mulr : 0 < z -> x < y / z ?<= if b = (x * z < y ?<= if b).
-Proof. by case: b => ? /=; rewrite lter_pdivl_mulr. Qed.
-
-Lemma lteif_pdivr_mulr : 0 < z -> y / z < x ?<= if b = (y < x * z ?<= if b).
-Proof. by case: b => ? /=; rewrite lter_pdivr_mulr. Qed.
-
-Lemma lteif_pdivl_mull : 0 < z -> x < z^-1 * y ?<= if b = (z * x < y ?<= if b).
-Proof. by case: b => ? /=; rewrite lter_pdivl_mull. Qed.
-
-Lemma lteif_pdivr_mull : 0 < z -> z^-1 * y < x ?<= if b = (y < z * x ?<= if b).
-Proof. by case: b => ? /=; rewrite lter_pdivr_mull. Qed.
-
-Lemma lteif_ndivl_mulr : z < 0 -> x < y / z ?<= if b = (y < x * z ?<= if b).
-Proof. by case: b => ? /=; rewrite lter_ndivl_mulr. Qed.
-
-Lemma lteif_ndivr_mulr : z < 0 -> y / z < x ?<= if b = (x * z < y ?<= if b).
-Proof. by case: b => ? /=; rewrite lter_ndivr_mulr. Qed.
-
-Lemma lteif_ndivl_mull : z < 0 -> x < z^-1 * y ?<= if b = (y < z * x ?<= if b).
-Proof. by case: b => ? /=; rewrite lter_ndivl_mull. Qed.
-
-Lemma lteif_ndivr_mull : z < 0 -> z^-1 * y < x ?<= if b = (z * x < y ?<= if b).
-Proof. by case: b => ? /=; rewrite lter_ndivr_mull. Qed.
-
-End LteifField.
-
 Section IntervalNumDomain.
 
 Variable R : numFieldType.
 Implicit Types x : R.
 
-Lemma mem0_itvcc_xNx x : (0 \in `[-x, x]) = (0 <= x).
+Lemma mem0_itvcc_xNx x : (0 \in `[- x, x]) = (0 <= x).
 Proof. by rewrite itv_boundlr [in LHS]/<=%O /= oppr_le0 andbb. Qed.
 
-Lemma mem0_itvoo_xNx x : 0 \in `](-x), x[ = (0 < x).
+Lemma mem0_itvoo_xNx x : 0 \in `](- x), x[ = (0 < x).
 Proof. by rewrite itv_boundlr [in LHS]/<=%O /= oppr_lt0 andbb. Qed.
 
-Lemma itv_splitI a b x :
-  x \in Interval a b = (x \in Interval a +oo) && (x \in Interval -oo b).
-Proof. by rewrite !itv_boundlr ?andbT. Qed.
-
 Lemma oppr_itv ba bb (xa xb x : R) :
-  (-x \in Interval (BRight_if ba xa) (BRight_if bb xb)) =
-  (x \in Interval (BRight_if (~~ bb) (- xb)) (BRight_if (~~ ba) (-xa))).
+  (- x \in Interval (BSide ba xa) (BSide bb xb)) =
+  (x \in Interval (BSide (~~ bb) (- xb)) (BSide (~~ ba) (- xa))).
 Proof.
 by rewrite !itv_boundlr /<=%O /= !implybF negbK andbC lteif_oppl lteif_oppr.
 Qed.
 
-Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[).
+Lemma oppr_itvoo (a b x : R) : (- x \in `]a, b[) = (x \in `](- b), (- a)[).
 Proof. exact: oppr_itv. Qed.
 
-Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]).
+Lemma oppr_itvco (a b x : R) : (- x \in `[a, b[) = (x \in `](- b), (- a)]).
 Proof. exact: oppr_itv. Qed.
 
-Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[).
+Lemma oppr_itvoc (a b x : R) : (- x \in `]a, b]) = (x \in `[(- b), (- a)[).
 Proof. exact: oppr_itv. Qed.
 
-Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]).
+Lemma oppr_itvcc (a b x : R) : (- x \in `[a, b]) = (x \in `[(- b), (- a)]).
 Proof. exact: oppr_itv. Qed.
 
 End IntervalNumDomain.
@@ -903,10 +618,10 @@ Variable R : realFieldType.
 
 Local Notation mid x y := ((x + y) / 2%:R).
 
-Lemma mid_in_itv : forall ba bb (xa xb : R), xa < xb ?<= if ~~ ba && bb ->
-  mid xa xb \in Interval (BRight_if ba xa) (BRight_if bb xb).
+Lemma mid_in_itv : forall ba bb (xa xb : R), xa < xb ?<= if ba && ~~ bb ->
+  mid xa xb \in Interval (BSide ba xa) (BSide bb xb).
 Proof.
-by move=> [] [] xa xb /= ?; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltW.
+by move=> [] [] xa xb /= ?; apply/itv_dec; rewrite /= ?midf_lte // ?ltW.
 Qed.
 
 Lemma mid_in_itvoo : forall (xa xb : R), xa < xb -> mid xa xb \in `]xa, xb[.
@@ -923,7 +638,7 @@ End IntervalField.
 
 Module mc_1_11.
 
-Local Notation lersif x y b := (lteif x y (~~ b)) (only parsing).
+Local Notation lersif x y b := (Order.lteif x y (~~ b)) (only parsing).
 
 Local Notation "x <= y ?< 'if' b" := (x < y ?<= if ~~ b)
   (at level 70, y at next level, only parsing) : ring_scope.
@@ -1037,7 +752,7 @@ Proof. exact: lteif_nmul2r. Qed.
 
 Lemma real_lersifN x y b : x \is Num.real -> y \is Num.real ->
   x <= y ?< if ~~b = ~~ (y <= x ?< if b).
-Proof. exact: real_lteifN. Qed.
+Proof. exact: real_lteifNE. Qed.
 
 Lemma real_lersif_norml b x y :
   x \is Num.real ->
@@ -1059,7 +774,7 @@ Section LersifOrdered.
 Variable (R : realDomainType) (b : bool) (x y z e : R).
 
 Lemma lersifN : (x <= y ?< if ~~ b) = ~~ (y <= x ?< if b).
-Proof. exact: lteifN. Qed.
+Proof. exact: lteifNE. Qed.
 
 Lemma lersif_norml :
   (`|x| <= y ?< if b) = (- y <= x ?< if b) && (x <= y ?< if b).
@@ -1125,17 +840,40 @@ Section IntervalPo.
 
 Variable R : numDomainType.
 
-Lemma lersif_in_itv ba bb (xa xb x : R) :
-  x \in Interval (BRight_if ba xa) (BRight_if bb xb) ->
-        xa <= xb ?< if ba || ~~ bb.
-Proof. by move/lteif_in_itv; rewrite negb_or negbK. Qed.
+Implicit Types (x xa xb : R).
+
+Lemma lersif_in_itv ba bb xa xb x :
+  x \in Interval (BSide ba xa) (BSide bb xb) -> xa <= xb ?< if ~~ ba || bb.
+Proof. by move/lt_in_itv; rewrite negb_or negbK. Qed.
+
+Lemma itv_gte ba xa bb xb :
+  xb <= xa ?< if ba && ~~ bb -> Interval (BSide ba xa) (BSide bb xb) =i pred0.
+Proof. by move=> ?; apply: itv_ge; rewrite /<%O /= lteifNF. Qed.
+
+Lemma ltr_in_itv ba bb xa xb x :
+  ~~ ba || bb -> x \in Interval (BSide ba xa) (BSide bb xb) -> xa < xb.
+Proof. by move=> bab /lersif_in_itv; rewrite bab. Qed.
+
+Lemma ler_in_itv ba bb xa xb x :
+  x \in Interval (BSide ba xa) (BSide bb xb) -> xa <= xb.
+Proof. by move/lt_in_itv/lteifW. Qed.
 
 End IntervalPo.
 
+Lemma itv_splitU2 (R : realDomainType) (x : R) a b :
+  x \in Interval a b ->
+  forall y, y \in Interval a b =
+    [|| y \in Interval a (BLeft x), y == x | y \in Interval (BRight x) b].
+Proof. exact: itv_splitUeq. Qed.
+
 End mc_1_11.
 
+(* Use `Order.lteif` instead of `lteif`. (`deprecate` does not accept a       *)
+(* qualified name.)                                                           *)
+Local Notation lteif := Order.lteif (only parsing).
+
 Notation "@ 'lersif'" :=
-  ((fun _ (R : numDomainType) x y b => @lteif _ R x y (~~ b))
+  ((fun _ (R : numDomainType) x y b => @Order.lteif _ R x y (~~ b))
      (deprecate lersif lteif))
     (at level 10, only parsing).
 
@@ -1351,7 +1089,7 @@ Notation "@ 'lersif_nmul2r'" :=
 Notation lersif_nmul2r := (fun b => @lersif_nmul2r _ b _) (only parsing).
 
 Notation "@ 'real_lersifN'" :=
-  ((fun _ => @mc_1_11.real_lersifN) (deprecate real_lersifN real_lteifN))
+  ((fun _ => @mc_1_11.real_lersifN) (deprecate real_lersifN real_lteifNE))
     (at level 10, only parsing).
 
 Notation real_lersifN := (@real_lersifN _ _ _) (only parsing).
@@ -1381,7 +1119,7 @@ Notation lersif_nnormr := (fun x => @lersif_nnormr _ _ x _) (only parsing).
 (* LersifOrdered *)
 
 Notation "@ 'lersifN'" :=
-  ((fun _ => @mc_1_11.lersifN) (deprecate lersifN lteifN))
+  ((fun _ => @mc_1_11.lersifN) (deprecate lersifN lteifNE))
     (at level 10, only parsing).
 
 Notation lersifN := (@lersifN _) (only parsing).
@@ -1502,9 +1240,32 @@ Notation "@ 'lersif_in_itv'" :=
 
 Notation lersif_in_itv := (@lersif_in_itv _ _ _ _ _ _) (only parsing).
 
+Notation "@ 'itv_gte'" :=
+  ((fun _ => @mc_1_11.itv_gte) (deprecate itv_gte itv_ge))
+    (at level 10, only parsing).
+
+Notation itv_gte := (@itv_gte _ _ _ _ _) (only parsing).
+
+Notation "@ 'ltr_in_itv'" :=
+  ((fun _ => @mc_1_11.ltr_in_itv) (deprecate ltr_in_itv lt_in_itv))
+    (at level 10, only parsing).
+
+Notation ltr_in_itv := (@ltr_in_itv _ _ _ _ _ _) (only parsing).
+
+Notation "@ 'ler_in_itv'" :=
+  ((fun _ => @mc_1_11.ler_in_itv) (deprecate ler_in_itv lt_in_itv))
+    (at level 10, only parsing).
+
+Notation ler_in_itv := (@ler_in_itv _ _ _ _ _ _) (only parsing).
+
+Notation "@ 'itv_splitU2'" :=
+  ((fun _ => @mc_1_11.itv_splitU2) (deprecate itv_splitU2 itv_splitUeq))
+    (at level 10, only parsing).
+
+Notation itv_splitU2 := (@itv_splitU2 _ _ _ _) (only parsing).
+
 (* `itv_intersection` accepts any `numDomainType` but `Order.meet` accepts    *)
 (* only `realDomainType`. Use `Order.meet` instead of `itv_meet`.             *)
-(* (`deprecate` does not accept a qualified name.)                            *)
 Notation "@ 'itv_intersection'" :=
   ((fun _ (R : realDomainType) => @Order.meet _ [latticeType of interval R])
      (deprecate itv_intersection itv_meet))
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index e09ba9b..2ebbdcc 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -80,11 +80,11 @@ From mathcomp Require Import ssralg poly.
 (*   [rcfType of T for S]                                                     *)
 (*                  == T-clone of the realClosedFieldType structure S.        *)
 (*                                                                            *)
-(* The ordering symbols and notations (<, <=, >, >=, _ <= _ ?= iff _, >=<,    *)
-(* and ><) and lattice operations (meet and join) defined in order.v are      *)
-(* redefined for the ring_display in the ring_scope (%R). 0-ary ordering      *)
-(* symbols for the ring_display have the suffix "%R", e.g., <%R. All the      *)
-(* other ordering notations are the same as order.v.                          *)
+(* The ordering symbols and notations (<, <=, >, >=, _ <= _ ?= iff _,         *)
+(* _ < _ ?<= if _, >=<, and ><) and lattice operations (meet and join)        *)
+(* defined in order.v are redefined for the ring_display in the ring_scope    *)
+(* (%R). 0-ary ordering symbols for the ring_display have the suffix "%R",    *)
+(* e.g., <%R. All the other ordering notations are the same as order.v.       *)
 (*                                                                            *)
 (* Over these structures, we have the following operations                    *)
 (*             `|x| == norm of x.                                             *)
@@ -387,6 +387,9 @@ Notation "@ 'gtr' R" := (@Order.gt ring_display R)
 Notation lerif := (@Order.leif ring_display _) (only parsing).
 Notation "@ 'lerif' R" := (@Order.leif ring_display R)
   (at level 10, R at level 8, only parsing) : fun_scope.
+Notation lterif := (@Order.lteif ring_display _) (only parsing).
+Notation "@ 'lteif' R" := (@Order.lteif ring_display R)
+  (at level 10, R at level 8, only parsing) : fun_scope.
 Notation comparabler := (@Order.comparable ring_display _) (only parsing).
 Notation "@ 'comparabler' R" := (@Order.comparable ring_display R)
   (at level 10, R at level 8, only parsing) : fun_scope.
@@ -416,6 +419,7 @@ Notation lt := ltr (only parsing).
 Notation ge := ger (only parsing).
 Notation gt := gtr (only parsing).
 Notation leif := lerif (only parsing).
+Notation lteif := lterif (only parsing).
 Notation comparable := comparabler (only parsing).
 Notation sg := sgr.
 Notation max := maxr.
@@ -448,6 +452,7 @@ Notation ">=%R" := ge : fun_scope.
 Notation "<%R" := lt : fun_scope.
 Notation ">%R" := gt : fun_scope.
 Notation "<?=%R" := leif : fun_scope.
+Notation "<?<=%R" := lteif : fun_scope.
 Notation ">=<%R" := comparable : fun_scope.
 Notation "><%R" := (fun x y => ~~ (comparable x y)) : fun_scope.
 
@@ -483,6 +488,10 @@ Notation "x <= y ?= 'iff' C" := (lerif x y C) : ring_scope.
 Notation "x <= y ?= 'iff' C :> R" := ((x : R) <= (y : R) ?= iff C)
   (only parsing) : ring_scope.
 
+Notation "x < y ?<= 'if' C" := (lterif x y C) : ring_scope.
+Notation "x < y ?<= 'if' C :> R" := ((x : R) < (y : R) ?<= if C)
+  (only parsing) : ring_scope.
+
 Notation ">=< x" := (comparable x) : ring_scope.
 Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : ring_scope.
 Notation "x >=< y" := (comparable x y) : ring_scope.
@@ -3313,6 +3322,94 @@ congr (leif _ _ _): (leif_pmul Ei_ge0 m1ge0 (leE12 i Pi) le_m12).
 by rewrite mulf_eq0 -!orbA; congr (_ || _); rewrite !orb_andr orbA orbb.
 Qed.
 
+(* lteif *)
+
+Lemma subr_lteifr0 C x y : (y - x < 0 ?<= if C) = (y < x ?<= if C).
+Proof. by case: C => /=; rewrite subr_lte0. Qed.
+
+Lemma subr_lteif0r C x y : (0 < y - x ?<= if C) = (x < y ?<= if C).
+Proof. by case: C => /=; rewrite subr_gte0. Qed.
+
+Definition subr_lteif0 := (subr_lteifr0, subr_lteif0r).
+
+Lemma lteif01 C : 0 < 1 ?<= if C :> R.
+Proof. by case: C; rewrite /= lter01. Qed.
+
+Lemma lteif_oppl C x y : - x < y ?<= if C = (- y < x ?<= if C).
+Proof. by case: C; rewrite /= lter_oppl. Qed.
+
+Lemma lteif_oppr C x y : x < - y ?<= if C = (y < - x ?<= if C).
+Proof. by case: C; rewrite /= lter_oppr. Qed.
+
+Lemma lteif_0oppr C x : 0 < - x ?<= if C = (x < 0 ?<= if C).
+Proof. by case: C; rewrite /= (oppr_ge0, oppr_gt0). Qed.
+
+Lemma lteif_oppr0 C x : - x < 0 ?<= if C = (0 < x ?<= if C).
+Proof. by case: C; rewrite /= (oppr_le0, oppr_lt0). Qed.
+
+Lemma lteif_opp2 C : {mono -%R : x y /~ x < y ?<= if C :> R}.
+Proof. by case: C => ? ?; rewrite /= lter_opp2. Qed.
+
+Definition lteif_oppE := (lteif_0oppr, lteif_oppr0, lteif_opp2).
+
+Lemma lteif_add2l C x : {mono +%R x : y z / y < z ?<= if C}.
+Proof. by case: C => ? ?; rewrite /= lter_add2. Qed.
+
+Lemma lteif_add2r C x : {mono +%R^~ x : y z / y < z ?<= if C}.
+Proof. by case: C => ? ?; rewrite /= lter_add2. Qed.
+
+Definition lteif_add2 := (lteif_add2l, lteif_add2r).
+
+Lemma lteif_subl_addr C x y z : (x - y < z ?<= if C) = (x < z + y ?<= if C).
+Proof. by case: C; rewrite /= lter_sub_addr. Qed.
+
+Lemma lteif_subr_addr C x y z : (x < y - z ?<= if C) = (x + z < y ?<= if C).
+Proof. by case: C; rewrite /= lter_sub_addr. Qed.
+
+Definition lteif_sub_addr := (lteif_subl_addr, lteif_subr_addr).
+
+Lemma lteif_subl_addl C x y z : (x - y < z ?<= if C) = (x < y + z ?<= if C).
+Proof. by case: C; rewrite /= lter_sub_addl. Qed.
+
+Lemma lteif_subr_addl C x y z : (x < y - z ?<= if C) = (z + x < y ?<= if C).
+Proof. by case: C; rewrite /= lter_sub_addl. Qed.
+
+Definition lteif_sub_addl := (lteif_subl_addl, lteif_subr_addl).
+
+Lemma lteif_pmul2l C x : 0 < x -> {mono *%R x : y z / y < z ?<= if C}.
+Proof. by case: C => ? ? ?; rewrite /= lter_pmul2l. Qed.
+
+Lemma lteif_pmul2r C x : 0 < x -> {mono *%R^~ x : y z / y < z ?<= if C}.
+Proof. by case: C => ? ? ?; rewrite /= lter_pmul2r. Qed.
+
+Lemma lteif_nmul2l C x : x < 0 -> {mono *%R x : y z /~ y < z ?<= if C}.
+Proof. by case: C => ? ? ?; rewrite /= lter_nmul2l. Qed.
+
+Lemma lteif_nmul2r C x : x < 0 -> {mono *%R^~ x : y z /~ y < z ?<= if C}.
+Proof. by case: C => ? ? ?; rewrite /= lter_nmul2r. Qed.
+
+Lemma lteif_nnormr C x y : y < 0 ?<= if ~~ C -> (`|x| < y ?<= if C) = false.
+Proof. by case: C => ?; rewrite /= lter_nnormr. Qed.
+
+Lemma real_lteifNE x y C : x \is Num.real -> y \is Num.real ->
+  x < y ?<= if ~~ C = ~~ (y < x ?<= if C).
+Proof. by move=> ? ?; rewrite comparable_lteifNE ?real_comparable. Qed.
+
+Lemma real_lteif_norml C x y :
+  x \is Num.real ->
+  (`|x| < y ?<= if C) = ((- y < x ?<= if C) && (x < y ?<= if C)).
+Proof. by case: C => ?; rewrite /= real_lter_norml. Qed.
+
+Lemma real_lteif_normr C x y :
+  y \is Num.real ->
+  (x < `|y| ?<= if C) = ((x < y ?<= if C) || (x < - y ?<= if C)).
+Proof. by case: C => ?; rewrite /= real_lter_normr. Qed.
+
+Lemma real_lteif_distl C x y e :
+  x - y \is real ->
+  (`|x - y| < e ?<= if C) = (y - e < x ?<= if C) && (x < y + e ?<= if C).
+Proof. by case: C => /= ?; rewrite real_lter_distl. Qed.
+
 (* Mean inequalities. *)
 
 Lemma real_leif_mean_square_scaled x y :
@@ -3621,17 +3718,51 @@ Proof. by rewrite !(fun_if GRing.inv) !(invr0, invrN, invr1). Qed.
 Lemma sgrV x : sgr x^-1 = sgr x.
 Proof. by rewrite /sgr invr_eq0 invr_lt0. Qed.
 
+(* lteif *)
+
+Lemma lteif_pdivl_mulr C z x y :
+  0 < z -> x < y / z ?<= if C = (x * z < y ?<= if C).
+Proof. by case: C => ? /=; rewrite lter_pdivl_mulr. Qed.
+
+Lemma lteif_pdivr_mulr C z x y :
+  0 < z -> y / z < x ?<= if C = (y < x * z ?<= if C).
+Proof. by case: C => ? /=; rewrite lter_pdivr_mulr. Qed.
+
+Lemma lteif_pdivl_mull C z x y :
+  0 < z -> x < z^-1 * y ?<= if C = (z * x < y ?<= if C).
+Proof. by case: C => ? /=; rewrite lter_pdivl_mull. Qed.
+
+Lemma lteif_pdivr_mull C z x y :
+  0 < z -> z^-1 * y < x ?<= if C = (y < z * x ?<= if C).
+Proof. by case: C => ? /=; rewrite lter_pdivr_mull. Qed.
+
+Lemma lteif_ndivl_mulr C z x y :
+  z < 0 -> x < y / z ?<= if C = (y < x * z ?<= if C).
+Proof. by case: C => ? /=; rewrite lter_ndivl_mulr. Qed.
+
+Lemma lteif_ndivr_mulr C z x y :
+  z < 0 -> y / z < x ?<= if C = (x * z < y ?<= if C).
+Proof. by case: C => ? /=; rewrite lter_ndivr_mulr. Qed.
+
+Lemma lteif_ndivl_mull C z x y :
+  z < 0 -> x < z^-1 * y ?<= if C = (y < z * x ?<= if C).
+Proof. by case: C => ? /=; rewrite lter_ndivl_mull. Qed.
+
+Lemma lteif_ndivr_mull C z x y :
+  z < 0 -> z^-1 * y < x ?<= if C = (z * x < y ?<= if C).
+Proof. by case: C => ? /=; rewrite lter_ndivr_mull. Qed.
+
 (* Interval midpoint. *)
 
 Local Notation mid x y := ((x + y) / 2%:R).
 
-Lemma midf_le x y : x <= y -> (x <= mid x y) * (mid x y  <= y).
+Lemma midf_le x y : x <= y -> (x <= mid x y) * (mid x y <= y).
 Proof.
 move=> lexy; rewrite ler_pdivl_mulr ?ler_pdivr_mulr ?ltr0Sn //.
 by rewrite !mulrDr !mulr1 ler_add2r ler_add2l.
 Qed.
 
-Lemma midf_lt x y : x < y -> (x < mid x y) * (mid x y  < y).
+Lemma midf_lt x y : x < y -> (x < mid x y) * (mid x y < y).
 Proof.
 move=> ltxy; rewrite ltr_pdivl_mulr ?ltr_pdivr_mulr ?ltr0Sn //.
 by rewrite !mulrDr !mulr1 ltr_add2r ltr_add2l.
@@ -3969,6 +4100,20 @@ Proof. by move=> even_n; rewrite real_exprn_odd_le0 ?num_real. Qed.
 Lemma exprn_odd_lt0 n x : odd n -> (x ^+ n < 0) = (x < 0).
 Proof. by move=> even_n; rewrite real_exprn_odd_lt0 ?num_real. Qed.
 
+(* lteif *)
+
+Lemma lteif_norml C x y :
+  (`|x| < y ?<= if C) = (- y < x ?<= if C) && (x < y ?<= if C).
+Proof. by case: C; rewrite /= lter_norml. Qed.
+
+Lemma lteif_normr C x y :
+  (x < `|y| ?<= if C) = (x < y ?<= if C) || (x < - y ?<= if C).
+Proof. by case: C; rewrite /= lter_normr. Qed.
+
+Lemma lteif_distl C x y e :
+  (`|x - y| < e ?<= if C) = (y - e < x ?<= if C) && (x < y + e ?<= if C).
+Proof. by case: C; rewrite /= lter_distl. Qed.
+
 (* Special lemmas for squares. *)
 
 Lemma sqr_ge0 x : 0 <= x ^+ 2. Proof. by rewrite exprn_even_ge0. Qed.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index da0e4d7..e4b956d 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -55,6 +55,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (*   @Order.ge          disp T     == >=%O    (in fun_scope)                  *)
 (*   @Order.gt          disp T     == >%O     (in fun_scope)                  *)
 (*   @Order.leif        disp T     == <?=%O   (in fun_scope)                  *)
+(*   @Order.lteif       disp T     == <?<=%O  (in fun_scope)                  *)
 (* For latticeType T                                                          *)
 (*   @Order.meet        disp T x y == x `&` y (in order_scope)                *)
 (*   @Order.join        disp T x y == x `|` y (in order_scope)                *)
@@ -79,6 +80,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (*            x >= y <-> x is greater than or equal to y (:= y <= x).         *)
 (*             x > y <-> x is greater than y (:= y < x).                      *)
 (*   x <= y ?= iff C <-> x is less than y, or equal iff C is true.            *)
+(*    x < y ?<= if C <-> x is smaller than y, and strictly if C is false.     *)
 (*           x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)).    *)
 (*            x >< y <-> x and y are incomparable (:= ~~ x >=< y).            *)
 (* For x, y of type T, where T is canonically a latticeType d:                *)
@@ -423,6 +425,11 @@ Reserved Notation "x >< y" (at level 70, no associativity).
 Reserved Notation ">< x" (at level 35).
 Reserved Notation ">< y :> T" (at level 35, y at next level).
 
+Reserved Notation "x < y ?<= 'if' c" (at level 70, y, c at next level,
+  format "x '[hv'  <  y '/'  ?<=  'if'  c ']'").
+Reserved Notation "x < y ?<= 'if' c :> T" (at level 70, y, c at next level,
+  format "x '[hv'  <  y '/'  ?<=  'if'  c  :> T ']'").
+
 (* Reserved notation for lattice operations. *)
 Reserved Notation "A `&` B"  (at level 48, left associativity).
 Reserved Notation "A `|` B" (at level 52, left associativity).
@@ -461,6 +468,10 @@ Reserved Notation "x <=^d y ?= 'iff' c" (at level 70, y, c at next level,
   format "x '[hv'  <=^d  y '/'  ?=  'iff'  c ']'").
 Reserved Notation "x <=^d y ?= 'iff' c :> T" (at level 70, y, c at next level,
   format "x '[hv'  <=^d  y '/'  ?=  'iff'  c  :> T ']'").
+Reserved Notation "x <^d y ?<= 'if' c" (at level 70, y, c at next level,
+  format "x '[hv'  <^d  y '/'  ?<=  'if'  c ']'").
+Reserved Notation "x <^d y ?<= 'if' c :> T" (at level 70, y, c at next level,
+  format "x '[hv'  <^d  y '/'  ?<=  'if'  c  :> T ']'").
 
 (* Reserved notation for dual lattice operations. *)
 Reserved Notation "A `&^d` B"  (at level 48, left associativity).
@@ -1065,6 +1076,8 @@ Definition leif (x y : T) C : Prop := ((x <= y) * ((x == y) = C))%type.
 
 Definition le_of_leif x y C (le_xy : @leif x y C) := le_xy.1 : le x y.
 
+Definition lteif x y C := if C then x <= y else x < y.
+
 Variant le_xor_gt (x y : T) :
   T -> T -> T -> T -> bool -> bool -> Set :=
   | LeNotGt of x <= y : le_xor_gt x y x x y y true false
@@ -1105,7 +1118,7 @@ Definition arg_max {I : finType}  := @extremum T I ge.
 
 End POrderDef.
 
-Prenex Implicits lt le leif.
+Prenex Implicits lt le leif lteif.
 Arguments ge {_ _}.
 Arguments gt {_ _}.
 Arguments min {_ _}.
@@ -1119,6 +1132,7 @@ Notation ">=%O" := ge : fun_scope.
 Notation "<%O" := lt : fun_scope.
 Notation ">%O" := gt : fun_scope.
 Notation "<?=%O" := leif : fun_scope.
+Notation "<?<=%O" := lteif : fun_scope.
 Notation ">=<%O" := comparable : fun_scope.
 Notation "><%O" := (fun x y => ~~ (comparable x y)) : fun_scope.
 
@@ -1154,6 +1168,10 @@ Notation "x <= y ?= 'iff' C" := (leif x y C) : order_scope.
 Notation "x <= y ?= 'iff' C :> T" := ((x : T) <= (y : T) ?= iff C)
   (only parsing) : order_scope.
 
+Notation "x < y ?<= 'if' C" := (lteif x y C) : order_scope.
+Notation "x < y ?<= 'if' C :> T" := ((x : T) < (y : T) ?<= if C)
+  (only parsing) : order_scope.
+
 Notation ">=< x" := (comparable x) : order_scope.
 Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : order_scope.
 Notation "x >=< y" := (comparable x y) : order_scope.
@@ -2493,6 +2511,7 @@ Notation dual_comparable := (@comparable (dual_display _) _).
 Notation dual_ge := (@ge (dual_display _) _).
 Notation dual_gt := (@gt (dual_display _) _).
 Notation dual_leif := (@leif (dual_display _) _).
+Notation dual_lteif := (@lteif (dual_display _) _).
 Notation dual_max := (@max (dual_display _) _).
 Notation dual_min := (@min (dual_display _) _).
 Notation dual_meet := (@meet (dual_display _) _).
@@ -2508,6 +2527,7 @@ Notation ">=^d%O" := dual_ge : fun_scope.
 Notation "<^d%O" := dual_lt : fun_scope.
 Notation ">^d%O" := dual_gt : fun_scope.
 Notation "<?=^d%O" := dual_leif : fun_scope.
+Notation "<?<=^d%O" := dual_lteif : fun_scope.
 Notation ">=<^d%O" := dual_comparable : fun_scope.
 Notation "><^d%O" := (fun x y => ~~ dual_comparable x y) : fun_scope.
 
@@ -2543,6 +2563,10 @@ Notation "x <=^d y ?= 'iff' C" := (<?=^d%O x y C) : order_scope.
 Notation "x <=^d y ?= 'iff' C :> T" := ((x : T) <=^d (y : T) ?= iff C)
   (only parsing) : order_scope.
 
+Notation "x <^d y ?<= 'if' C" := (<?<=^d%O x y C) : order_scope.
+Notation "x <^d y ?<= 'if' C :> T" := ((x : T) <^d (y : T) ?<= if C)
+  (only parsing) : order_scope.
+
 Notation ">=<^d x" := (>=<^d%O x) : order_scope.
 Notation ">=<^d x :> T" := (>=<^d (x : T)) (only parsing) : order_scope.
 Notation "x >=<^d y" := (>=<^d%O x y) : order_scope.
@@ -2808,6 +2832,8 @@ Proof. by case: comparableP. Qed.
 Lemma gt_comparable (x y : T) : y < x -> x >=< y.
 Proof. by case: comparableP. Qed.
 
+(* leif *)
+
 Lemma leifP x y C : reflect (x <= y ?= iff C) (if C then x == y else x < y).
 Proof.
 rewrite /leif le_eqVlt; apply: (iffP idP)=> [|[]].
@@ -2848,6 +2874,50 @@ Proof. by move=> /leifP; case: C comparableP => [] []. Qed.
 Lemma eqTleif x y C : x <= y ?= iff C -> C -> x = y.
 Proof. by move=> /eq_leif<-/eqP. Qed.
 
+(* lteif *)
+
+Lemma lteif_trans x y z C1 C2 :
+  x < y ?<= if C1 -> y < z ?<= if C2 -> x < z ?<= if C1 && C2.
+Proof.
+case: C1 C2 => [][];
+  [exact: le_trans | exact: le_lt_trans | exact: lt_le_trans | exact: lt_trans].
+Qed.
+
+Lemma lteif_anti C1 C2 x y :
+  (x < y ?<= if C1) && (y < x ?<= if C2) = C1 && C2 && (x == y).
+Proof. by case: C1 C2 => [][]; rewrite lte_anti. Qed.
+
+Lemma lteifxx x C : (x < x ?<= if C) = C.
+Proof. by case: C; rewrite /= ltexx. Qed.
+
+Lemma lteifNF x y C : y < x ?<= if ~~ C -> x < y ?<= if C = false.
+Proof. by case: C => [/lt_geF|/le_gtF]. Qed.
+
+Lemma lteifS x y C : x < y -> x < y ?<= if C.
+Proof. by case: C => //= /ltW. Qed.
+
+Lemma lteifT x y : x < y ?<= if true = (x <= y). Proof. by []. Qed.
+
+Lemma lteifF x y : x < y ?<= if false = (x < y). Proof. by []. Qed.
+
+Lemma lteif_orb x y : {morph lteif x y : p q / p || q}.
+Proof. by case=> [][] /=; case: comparableP. Qed.
+
+Lemma lteif_andb x y : {morph lteif x y : p q / p && q}.
+Proof. by case=> [][] /=; case: comparableP. Qed.
+
+Lemma lteif_imply C1 C2 x y : C1 ==> C2 -> x < y ?<= if C1 -> x < y ?<= if C2.
+Proof. by case: C1 C2 => [][] //= _ /ltW. Qed.
+
+Lemma lteifW C x y : x < y ?<= if C -> x <= y.
+Proof. by case: C => // /ltW. Qed.
+
+Lemma ltrW_lteif C x y : x < y -> x < y ?<= if C.
+Proof. by case: C => // /ltW. Qed.
+
+Lemma lteifN C x y : x < y ?<= if ~~ C -> ~~ (y < x ?<= if C).
+Proof. by case: C => /=; case: comparableP. Qed.
+
 (* min and max *)
 
 Lemma minElt x y : min x y = if x < y then x else y. Proof. by []. Qed.
@@ -2996,6 +3066,25 @@ Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
 Lemma comparable_maxKx : min x (max x y) = x.
 Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed.
 
+Lemma comparable_lteifNE C : x >=< y -> x < y ?<= if ~~ C = ~~ (y < x ?<= if C).
+Proof. by case: C => /=; case: comparableP. Qed.
+
+Lemma comparable_lteif_minr C :
+  (z < Order.min x y ?<= if C) = (z < x ?<= if C) && (z < y ?<= if C).
+Proof. by case: C; rewrite /= (comparable_le_minr, comparable_lt_minr). Qed.
+
+Lemma comparable_lteif_minl C :
+  (Order.min x y < z ?<= if C) = (x < z ?<= if C) || (y < z ?<= if C).
+Proof. by case: C; rewrite /= (comparable_le_minl, comparable_lt_minl). Qed.
+
+Lemma comparable_lteif_maxr C :
+  (z < Order.max x y ?<= if C) = (z < x ?<= if C) || (z < y ?<= if C).
+Proof. by case: C; rewrite /= (comparable_le_maxr, comparable_lt_maxr). Qed.
+
+Lemma comparable_lteif_maxl C :
+  (Order.max x y < z ?<= if C) = (x < z ?<= if C) && (y < z ?<= if C).
+Proof. by case: C; rewrite /= (comparable_le_maxl, comparable_lt_maxl). Qed.
+
 End Comparable2.
 
 Section Comparable3.
@@ -3799,6 +3888,27 @@ Definition lteIx := (leIx, ltIx).
 Definition ltexU := (lexU, ltxU).
 Definition lteUx := (@leUx _ T, ltUx).
 
+(* lteif *)
+
+Lemma lteifNE x y C : x < y ?<= if ~~ C = ~~ (y < x ?<= if C).
+Proof. by case: C => /=; case: leP. Qed.
+
+Lemma lteif_minr z x y C :
+  (z < Order.min x y ?<= if C) = (z < x ?<= if C) && (z < y ?<= if C).
+Proof. by case: C; rewrite /= (le_minr, lt_minr). Qed.
+
+Lemma lteif_minl z x y C :
+  (Order.min x y < z ?<= if C) = (x < z ?<= if C) || (y < z ?<= if C).
+Proof. by case: C; rewrite /= (le_minl, lt_minl). Qed.
+
+Lemma lteif_maxr z x y C :
+  (z < Order.max x y ?<= if C) = (z < x ?<= if C) || (z < y ?<= if C).
+Proof. by case: C; rewrite /= (le_maxr, lt_maxr). Qed.
+
+Lemma lteif_maxl z x y C :
+  (Order.max x y < z ?<= if C) = (x < z ?<= if C) && (y < z ?<= if C).
+Proof. by case: C; rewrite /= (le_maxl, lt_maxl). Qed.
+
 Section ArgExtremum.
 
 Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0).