Merge pull request #458 from pi8027/interval

The new interval library

3 files changed, 1347 insertions, 417 deletions

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 950546b..d6ea076 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -4,225 +4,805 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import div fintype bigop order ssralg finset fingroup.
 From mathcomp Require Import ssrnum.
 
-(*****************************************************************************)
-(* This file provide support for intervals in numerical and real domains.    *)
-(* The datatype (interval R) 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.                    *)
-(*    x \in i       == when i is a formal interval on a numeric domain,      *)
-(*                   \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 true        *)
-(*                                                                           *)
-(* We provide a set of notations to write intervals (see below)              *)
-(* `[a, b], `]a, b], ..., `]-oo, a], ..., `]-oo, +oo[                        *)
-(* We also provide the lemma subitvP which computes the inequalities one     *)
-(* needs to prove when trying to prove the inclusion of intervals.           *)
-(*                                                                           *)
-(* Remark that we cannot implement a boolean comparison test for intervals   *)
-(* on an arbitrary numeric domains, for this problem might be undecidable.   *)
-(* Note also that type (interval R) may contain several inhabitants coding   *)
-(* for the same interval. However, this pathological issues do nor arise     *)
-(* when R is a real domain: we could provide a specific theory for this      *)
-(* important case.                                                           *)
-(*                                                                           *)
-(* See also ``Formal proofs in real algebraic geometry: from ordered fields  *)
-(* to quantifier elimination'', LMCS journal, 2012                           *)
-(* by Cyril Cohen and Assia Mahboubi                                         *)
-(*                                                                           *)
-(* And "Formalized algebraic numbers: construction and first-order theory"   *)
-(* Cyril Cohen, PhD, 2012, section 4.3.                                      *)
-(*****************************************************************************)
+(******************************************************************************)
+(* 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 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.        *)
+(*                                                                            *)
+(* 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   *)
+(* (latticeType) whose meet and join are intersection and convex hull         *)
+(* respectively. They are distributive if T is an orderType.                  *)
+(*                                                                            *)
+(* We provide a set of notations to write intervals (see below)               *)
+(* `[a, b], `]a, b], ..., `]-oo, a], ..., `]-oo, +oo[                         *)
+(* We also provide the lemma subitvP which computes the inequalities one      *)
+(* needs to prove when trying to prove the inclusion of intervals.            *)
+(*                                                                            *)
+(* Remark that we cannot implement a boolean comparison test for intervals on *)
+(* an arbitrary ordered types, for this problem might be undecidable. Note    *)
+(* also that type (interval R) may contain several inhabitants coding for the *)
+(* same interval. However, this pathological issues do nor arise when R is a  *)
+(* real domain: we could provide a specific theory for this important case.   *)
+(*                                                                            *)
+(* See also ``Formal proofs in real algebraic geometry: from ordered fields   *)
+(* to quantifier elimination'', LMCS journal, 2012                            *)
+(* by Cyril Cohen and Assia Mahboubi                                          *)
+(*                                                                            *)
+(* And "Formalized algebraic numbers: construction and first-order theory"    *)
+(* Cyril Cohen, PhD, 2012, section 4.3.                                       *)
+(******************************************************************************)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Local Open Scope order_scope.
+Import Order.TTheory.
+
+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 *)
+Notation "`[ a , b ]" := (Interval (BLeft a) (BRight b))
+  (at level 0, a, b at level 9 , format "`[ a ,  b ]") : order_scope.
+Notation "`] a , b ]" := (Interval (BRight a) (BRight b))
+  (at level 0, a, b at level 9 , format "`] a ,  b ]") : order_scope.
+Notation "`[ a , b [" := (Interval (BLeft a) (BLeft b))
+  (at level 0, a, b at level 9 , format "`[ a ,  b [") : order_scope.
+Notation "`] a , b [" := (Interval (BRight a) (BLeft b))
+  (at level 0, a, b at level 9 , format "`] a ,  b [") : order_scope.
+Notation "`] '-oo' , b ]" := (Interval -oo (BRight b))
+  (at level 0, b at level 9 , format "`] '-oo' ,  b ]") : order_scope.
+Notation "`] '-oo' , b [" := (Interval -oo (BLeft b))
+  (at level 0, b at level 9 , format "`] '-oo' ,  b [") : order_scope.
+Notation "`[ a , '+oo' [" := (Interval (BLeft a) +oo)
+  (at level 0, a at level 9 , format "`[ a ,  '+oo' [") : order_scope.
+Notation "`] a , '+oo' [" := (Interval (BRight a) +oo)
+  (at level 0, a at level 9 , format "`] a ,  '+oo' [") : order_scope.
+Notation "`] -oo , '+oo' [" := (Interval -oo +oo)
+  (at level 0, format "`] -oo ,  '+oo' [") : order_scope.
+
+Notation "`[ a , b ]" := (Interval (BLeft a) (BRight b))
+  (at level 0, a, b at level 9 , format "`[ a ,  b ]") : ring_scope.
+Notation "`] a , b ]" := (Interval (BRight a) (BRight b))
+  (at level 0, a, b at level 9 , format "`] a ,  b ]") : ring_scope.
+Notation "`[ a , b [" := (Interval (BLeft a) (BLeft b))
+  (at level 0, a, b at level 9 , format "`[ a ,  b [") : ring_scope.
+Notation "`] a , b [" := (Interval (BRight a) (BLeft b))
+  (at level 0, a, b at level 9 , format "`] a ,  b [") : ring_scope.
+Notation "`] '-oo' , b ]" := (Interval -oo (BRight b))
+  (at level 0, b at level 9 , format "`] '-oo' ,  b ]") : ring_scope.
+Notation "`] '-oo' , b [" := (Interval -oo (BLeft b))
+  (at level 0, b at level 9 , format "`] '-oo' ,  b [") : ring_scope.
+Notation "`[ a , '+oo' [" := (Interval (BLeft a) +oo)
+  (at level 0, a at level 9 , format "`[ a ,  '+oo' [") : ring_scope.
+Notation "`] a , '+oo' [" := (Interval (BRight a) +oo)
+  (at level 0, a at level 9 , format "`] a ,  '+oo' [") : ring_scope.
+Notation "`] -oo , '+oo' [" := (Interval -oo +oo)
+  (at level 0, format "`] -oo ,  '+oo' [") : ring_scope.
+
+Fact itv_bound_display (disp : unit) : unit. Proof. exact. Qed.
+Fact interval_display (disp : unit) : unit. Proof. exact. Qed.
+
+Section IntervalEq.
+
+Variable T : eqType.
+
+Definition eq_itv_bound (b1 b2 : itv_bound T) : bool :=
+  match b1, b2 with
+    | BSide a x, BSide b y => (a == b) && (x == y)
+    | BInfty a, BInfty b => a == b
+    | _, _ => false
+  end.
+
+Lemma eq_itv_boundP : Equality.axiom eq_itv_bound.
+Proof.
+move=> b1 b2; apply: (iffP idP).
+- by move: b1 b2 => [a x|a][b y|b] => //= [/andP [/eqP -> /eqP ->]|/eqP ->].
+- by move=> <-; case: b1 => //= a x; rewrite !eqxx.
+Qed.
+
+Canonical itv_bound_eqMixin := EqMixin eq_itv_boundP.
+Canonical itv_bound_eqType := EqType (itv_bound T) itv_bound_eqMixin.
+
+Definition eqitv (x y : interval T) : bool :=
+  let: Interval x x' := x in
+  let: Interval y y' := y in (x == y) && (x' == y').
+
+Lemma eqitvP : Equality.axiom eqitv.
+Proof.
+move=> x y; apply: (iffP idP).
+- by move: x y => [x x'][y y'] => //= /andP [] /eqP -> /eqP ->.
+- by move=> <-; case: x => /= x x'; rewrite !eqxx.
+Qed.
+
+Canonical interval_eqMixin := EqMixin eqitvP.
+Canonical interval_eqType := EqType (interval T) interval_eqMixin.
+
+End IntervalEq.
+
+Module IntervalChoice.
+Section IntervalChoice.
+
+Variable T : choiceType.
+
+Lemma itv_bound_can :
+  cancel (fun b : itv_bound T =>
+            match b with BSide b x => (b, Some x) | BInfty b => (b, None) end)
+         (fun b =>
+            match b with (b, Some x) => BSide b x | (b, None) => BInfty _ b end).
+Proof. by case. Qed.
+
+Lemma interval_can :
+  @cancel _ (interval T)
+    (fun '(Interval b1 b2) => (b1, b2)) (fun '(b1, b2) => Interval b1 b2).
+Proof. by case. Qed.
+
+End IntervalChoice.
+
+Module Exports.
+
+Canonical itv_bound_choiceType (T : choiceType) :=
+  ChoiceType (itv_bound T) (CanChoiceMixin (@itv_bound_can T)).
+Canonical interval_choiceType (T : choiceType) :=
+  ChoiceType (interval T) (CanChoiceMixin (@interval_can T)).
+
+Canonical itv_bound_countType (T : countType) :=
+  CountType (itv_bound T) (CanCountMixin (@itv_bound_can T)).
+Canonical interval_countType (T : countType) :=
+  CountType (interval T) (CanCountMixin (@interval_can T)).
+
+Canonical itv_bound_finType (T : finType) :=
+  FinType (itv_bound T) (CanFinMixin (@itv_bound_can T)).
+Canonical interval_finType (T : finType) :=
+  FinType (interval T) (CanFinMixin (@interval_can T)).
+
+End Exports.
+
+End IntervalChoice.
+Export IntervalChoice.Exports.
+
+Section IntervalPOrder.
+
+Variable (disp : unit) (T : porderType disp).
+Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T).
+
+Definition le_bound b1 b2 :=
+  match b1, b2 with
+    | -oo, _ | _, +oo => true
+    | BSide b1 x1, BSide b2 x2 => x1 < x2 ?<= if b2 ==> b1
+    | _, _ => false
+  end.
+
+Definition lt_bound b1 b2 :=
+  match b1, b2 with
+    | -oo, +oo | -oo, BSide _ _ | BSide _ _, +oo => true
+    | BSide b1 x1, BSide b2 x2 => x1 < x2 ?<= if b1 && ~~ b2
+    | _, _ => false
+  end.
+
+Lemma lt_bound_def b1 b2 : lt_bound b1 b2 = (b2 != b1) && le_bound b1 b2.
+Proof. by case: b1 b2 => [[]?|[]][[]?|[]] //=; rewrite lt_def. Qed.
+
+Lemma le_bound_refl : reflexive le_bound.
+Proof. by move=> [[]?|[]] /=. Qed.
+
+Lemma le_bound_anti : antisymmetric le_bound.
+Proof. by case=> [[]?|[]] [[]?|[]] //=; case: comparableP => // ->. Qed.
+
+Lemma le_bound_trans : transitive le_bound.
+Proof.
+by case=> [[]?|[]] [[]?|[]] [[]?|[]] lexy leyz //;
+  apply: (lteif_imply _ (lteif_trans lexy leyz)).
+Qed.
+
+Definition itv_bound_porderMixin :=
+  LePOrderMixin lt_bound_def le_bound_refl le_bound_anti le_bound_trans.
+Canonical itv_bound_porderType :=
+  POrderType (itv_bound_display disp) (itv_bound T) itv_bound_porderMixin.
+
+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 :=
+  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.
+
+Lemma subitv_anti : antisymmetric subitv.
+Proof.
+by case=> [? ?][? ?]; rewrite andbACA => /andP[] /le_anti -> /le_anti ->.
+Qed.
+
+Lemma subitv_trans : transitive subitv.
+Proof.
+case=> [yl yr][xl xr][zl zr] /andP [Hl Hr] /andP [Hl' Hr'] /=.
+by rewrite (le_trans Hl' Hl) (le_trans Hr Hr').
+Qed.
+
+Definition interval_porderMixin :=
+  LePOrderMixin (fun _ _ => erefl) subitv_refl subitv_anti subitv_trans.
+Canonical interval_porderType :=
+  POrderType (interval_display disp) (interval T) interval_porderMixin.
+
+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 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 subitvPr bl b1r b2r :
+  b1r <= b2r -> {subset Interval bl b1r <= Interval bl b2r}.
+Proof. by move=> ?; apply: subitvP; rewrite subitvE 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 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 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
+     | BSide b lb => lb < x ?<= if b
+     | BInfty b => b
+   end *
+   match u return Prop with
+     | 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).
+Proof. by move=> ? [[? ?|[]][? ?|[]]]; apply: (iffP andP); case. Qed.
+
+Arguments itv_dec {x i}.
+
+(* we compute a set of rewrite rules associated to an interval *)
+Definition itv_rewrite i x : Type :=
+  let: Interval l u := i in
+    (match l with
+       | 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 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 b : bool, unkeyed b = false
+     end *
+     match l, u with
+       | BLeft a, BRight b =>
+         (a <= b) * (b < a = false) * (a \in `[a, b]) * (b \in `[a, b])
+       | BLeft a, BLeft b =>
+         (a <= b) * (a < b) * (b <= a = false) * (b < a = false)
+         * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b])
+       | BRight a, BRight b =>
+         (a <= b) * (a < b) * (b <= a = false) * (b < a = false)
+         * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b])
+       | BRight a, BLeft b =>
+         (a <= b) * (a < b) * (b <= a = false) * (b < a = false)
+         * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b])
+       | _, _ => forall x : T, x == x
+     end)%type.
+
+Lemma itvP x i : x \in i -> itv_rewrite i x.
+Proof.
+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].
+
+End IntervalPOrder.
+
+Section IntervalLattice.
+
+Variable (disp : unit) (T : latticeType disp).
+Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T).
+
+Definition bound_meet bl br : itv_bound T :=
+  match bl, br with
+    | -oo, _ | _, -oo => -oo
+    | +oo, b | b, +oo => b
+    | 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
+    | 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 BSide.
+by case: lcomparableP; rewrite ?orbF // orbC.
+Qed.
+
+Lemma bound_joinC : commutative bound_join.
+Proof.
+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 BSide.
+by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->];
+  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; congr BSide.
+by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->];
+  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 => [? ?|[]][? ?|[]] //=;
+  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 => [? ?|[]][? ?|[]] //=;
+  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).
+Proof.
+by case: b1 b2 => [[]?|[]][[]?|[]] //=;
+  rewrite [LHS]/<=%O /eq_op /= ?eqxx //= -leEmeet; case: lcomparableP.
+Qed.
+
+Definition itv_bound_latticeMixin :=
+  LatticeMixin bound_meetC bound_joinC bound_meetA bound_joinA
+               bound_joinKI bound_meetKU bound_leEmeet.
+Canonical itv_bound_latticeType :=
+  LatticeType (itv_bound T) itv_bound_latticeMixin.
+
+Lemma bound_le0x b : -oo <= b. Proof. by []. Qed.
+
+Lemma bound_lex1 b : b <= +oo. Proof. by case: b => [|[]]. Qed.
+
+Canonical itv_bound_bLatticeType :=
+  BLatticeType (itv_bound T) (BottomMixin bound_le0x).
+
+Canonical itv_bound_tbLatticeType :=
+  TBLatticeType (itv_bound T) (TopMixin bound_lex1).
+
+Definition itv_meet i1 i2 : interval T :=
+  let: Interval b1l b1r := i1 in
+  let: Interval b2l b2r := i2 in Interval (b1l `|` b2l) (b1r `&` b2r).
+
+Definition itv_join i1 i2 : interval T :=
+  let: Interval b1l b1r := i1 in
+  let: Interval b2l b2r := i2 in Interval (b1l `&` b2l) (b1r `|` b2r).
+
+Lemma itv_meetC : commutative itv_meet.
+Proof. by case=> [? ?][? ?] /=; rewrite meetC joinC. Qed.
+
+Lemma itv_joinC : commutative itv_join.
+Proof. by case=> [? ?][? ?] /=; rewrite meetC joinC. Qed.
+
+Lemma itv_meetA : associative itv_meet.
+Proof. by case=> [? ?][? ?][? ?] /=; rewrite meetA joinA. Qed.
+
+Lemma itv_joinA : associative itv_join.
+Proof. by case=> [? ?][? ?][? ?] /=; rewrite meetA joinA. Qed.
+
+Lemma itv_meetKU i2 i1 : itv_join i1 (itv_meet i1 i2) = i1.
+Proof. by case: i1 i2 => [? ?][? ?] /=; rewrite meetKU joinKI. Qed.
+
+Lemma itv_joinKI i2 i1 : itv_meet i1 (itv_join i1 i2) = i1.
+Proof. by case: i1 i2 => [? ?][? ?] /=; rewrite meetKU joinKI. Qed.
+
+Lemma itv_leEmeet i1 i2 : (i1 <= i2) = (itv_meet i1 i2 == i1).
+Proof. by case: i1 i2 => [? ?][? ?]; rewrite /eq_op /= eq_meetl eq_joinl. Qed.
+
+Definition interval_latticeMixin :=
+  LatticeMixin itv_meetC itv_joinC itv_meetA itv_joinA
+               itv_joinKI itv_meetKU itv_leEmeet.
+Canonical interval_latticeType :=
+  LatticeType (interval T) interval_latticeMixin.
+
+Lemma itv_le0x i : Interval +oo -oo <= i. Proof. by case: i => [[|[]]]. Qed.
+
+Lemma itv_lex1 i : i <= `]-oo, +oo[. Proof. by case: i => [?[|[]]]. Qed.
+
+Canonical interval_bLatticeType :=
+  BLatticeType (interval T) (BottomMixin itv_le0x).
+
+Canonical interval_tbLatticeType :=
+  TBLatticeType (interval T) (TopMixin itv_lex1).
+
+Lemma in_itvI x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2).
+Proof. exact: lexI. Qed.
+
+End IntervalLattice.
+
+Section IntervalTotal.
+
+Variable (disp : unit) (T : orderType disp).
+Implicit Types (x y z : T) (i : interval T).
+
+Lemma itv_bound_totalMixin : totalLatticeMixin [latticeType of itv_bound T].
+Proof. by move=> [[]?|[]][[]?|[]]; rewrite /<=%O //=; case: ltgtP. Qed.
+
+Canonical itv_bound_distrLatticeType :=
+  DistrLatticeType (itv_bound T) itv_bound_totalMixin.
+Canonical itv_bound_bDistrLatticeType := [bDistrLatticeType of itv_bound T].
+Canonical itv_bound_tbDistrLatticeType := [tbDistrLatticeType of itv_bound T].
+Canonical itv_bound_orderType := OrderType (itv_bound T) itv_bound_totalMixin.
+
+Lemma itv_meetUl : @left_distributive (interval T) _ Order.meet Order.join.
+Proof.
+by move=> [? ?][? ?][? ?]; rewrite /Order.meet /Order.join /= -meetUl -joinIl.
+Qed.
+
+Canonical interval_distrLatticeType :=
+  DistrLatticeType (interval T) (DistrLatticeMixin itv_meetUl).
+Canonical interval_bDistrLatticeType := [bDistrLatticeType of interval T].
+Canonical interval_tbDistrLatticeType := [tbDistrLatticeType of interval T].
+
+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.
+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_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].
+Proof.
+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.
+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 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.
+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 b13r (le_trans b12r b23r).
+- 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.
+
 Local Open Scope ring_scope.
-Import Order.TTheory GRing.Theory Num.Theory.
+Import GRing.Theory Num.Theory.
+
+Section IntervalNumDomain.
+
+Variable R : numFieldType.
+Implicit Types x : R.
+
+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).
+Proof. by rewrite itv_boundlr [in LHS]/<=%O /= oppr_lt0 andbb. Qed.
+
+Lemma oppr_itv ba bb (xa xb x : R) :
+  (- 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)[).
+Proof. exact: oppr_itv. Qed.
+
+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)[).
+Proof. exact: oppr_itv. Qed.
+
+Lemma oppr_itvcc (a b x : R) : (- x \in `[a, b]) = (x \in `[(- b), (- a)]).
+Proof. exact: oppr_itv. Qed.
+
+End IntervalNumDomain.
+
+Section IntervalField.
+
+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 (BSide ba xa) (BSide bb xb).
+Proof.
+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[.
+Proof. by move=> xa xb ?; apply: mid_in_itv. Qed.
+
+Lemma mid_in_itvcc : forall (xa xb : R), xa <= xb -> mid xa xb \in `[xa, xb].
+Proof. by move=> xa xb ?; apply: mid_in_itv. Qed.
+
+End IntervalField.
+
+(******************************************************************************)
+(* Compatibility layer                                                        *)
+(******************************************************************************)
+
+Module mc_1_11.
+
+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.
+
 Section LersifPo.
 
 Variable R : numDomainType.
 Implicit Types (b : bool) (x y z : R).
 
-Definition lersif (x y : R) b := if b then x < y else x <= y.
-
-Local Notation "x <= y ?< 'if' b" := (lersif x y b)
-  (at level 70, y at next level,
-  format "x '[hv'  <=  y '/'  ?<  'if'  b ']'") : ring_scope.
-
 Lemma subr_lersifr0 b (x y : R) : (y - x <= 0 ?< if b) = (y <= x ?< if b).
-Proof. by case: b => /=; rewrite subr_lte0. Qed.
+Proof. exact: subr_lteifr0. Qed.
 
 Lemma subr_lersif0r b (x y : R) : (0 <= y - x ?< if b) = (x <= y ?< if b).
-Proof. by case: b => /=; rewrite subr_gte0. Qed.
+Proof. exact: subr_lteif0r. Qed.
 
 Definition subr_lersif0 := (subr_lersifr0, subr_lersif0r).
 
 Lemma lersif_trans x y z b1 b2 :
   x <= y ?< if b1 -> y <= z ?< if b2 -> x <= z ?< if b1 || b2.
-Proof.
-by case: b1 b2 => [] [];
-  [apply: lt_trans | apply: lt_le_trans | apply: le_lt_trans | apply: le_trans].
-Qed.
+Proof. by rewrite negb_or; exact: lteif_trans. Qed.
 
-Lemma lersif01 b : 0 <= 1 ?< if b.
-Proof. by case: b; apply lter01. Qed.
+Lemma lersif01 b : (0 : R) <= 1 ?< if b. Proof. exact: lteif01. Qed.
 
 Lemma lersif_anti b1 b2 x y :
   (x <= y ?< if b1) && (y <= x ?< if b2) =
   if b1 || b2 then false else x == y.
-Proof. by case: b1 b2 => [] []; rewrite lte_anti. Qed.
+Proof. by rewrite lteif_anti -negb_or; case: orb. Qed.
 
-Lemma lersifxx x b : (x <= x ?< if b) = ~~ b.
-Proof. by case: b; rewrite /= ltexx. Qed.
+Lemma lersifxx x b : (x <= x ?< if b) = ~~ b. Proof. exact: lteifxx. Qed.
 
 Lemma lersifNF x y b : y <= x ?< if ~~ b -> x <= y ?< if b = false.
-Proof. by case: b => /= [/le_gtF|/lt_geF]. Qed.
+Proof. exact: lteifNF. Qed.
 
 Lemma lersifS x y b : x < y -> x <= y ?< if b.
-Proof. by case: b => //= /ltW. Qed.
+Proof. exact: lteifS. Qed.
 
 Lemma lersifT x y : x <= y ?< if true = (x < y). Proof. by []. Qed.
 
 Lemma lersifF x y : x <= y ?< if false = (x <= y). Proof. by []. Qed.
 
 Lemma lersif_oppl b x y : - x <= y ?< if b = (- y <= x ?< if b).
-Proof. by case: b; apply lter_oppl. Qed.
+Proof. exact: lteif_oppl. Qed.
 
 Lemma lersif_oppr b x y : x <= - y ?< if b = (y <= - x ?< if b).
-Proof. by case: b; apply lter_oppr. Qed.
+Proof. exact: lteif_oppr. Qed.
 
 Lemma lersif_0oppr b x : 0 <= - x ?< if b = (x <= 0 ?< if b).
-Proof. by case: b; apply (oppr_ge0, oppr_gt0). Qed.
+Proof. exact: lteif_0oppr. Qed.
 
 Lemma lersif_oppr0 b x : - x <= 0 ?< if b = (0 <= x ?< if b).
-Proof. by case: b; apply (oppr_le0, oppr_lt0). Qed.
+Proof. exact: lteif_oppr0. Qed.
 
-Lemma lersif_opp2 b : {mono -%R : x y /~ x <= y ?< if b}.
-Proof. by case: b; apply lter_opp2. Qed.
+Lemma lersif_opp2 b : {mono (-%R : R -> R) : x y /~ x <= y ?< if b}.
+Proof. exact: lteif_opp2. Qed.
 
 Definition lersif_oppE := (lersif_0oppr, lersif_oppr0, lersif_opp2).
 
 Lemma lersif_add2l b x : {mono +%R x : y z / y <= z ?< if b}.
-Proof. by case: b => ? ?; apply lter_add2. Qed.
+Proof. exact: lteif_add2l. Qed.
 
 Lemma lersif_add2r b x : {mono +%R^~ x : y z / y <= z ?< if b}.
-Proof. by case: b => ? ?; apply lter_add2. Qed.
+Proof. exact: lteif_add2r. Qed.
 
 Definition lersif_add2 := (lersif_add2l, lersif_add2r).
 
 Lemma lersif_subl_addr b x y z : (x - y <= z ?< if b) = (x <= z + y ?< if b).
-Proof. by case: b; apply lter_sub_addr. Qed.
+Proof. exact: lteif_subl_addr. Qed.
 
 Lemma lersif_subr_addr b x y z : (x <= y - z ?< if b) = (x + z <= y ?< if b).
-Proof. by case: b; apply lter_sub_addr. Qed.
+Proof. exact: lteif_subr_addr. Qed.
 
 Definition lersif_sub_addr := (lersif_subl_addr, lersif_subr_addr).
 
 Lemma lersif_subl_addl b x y z : (x - y <= z ?< if b) = (x <= y + z ?< if b).
-Proof. by case: b; apply lter_sub_addl. Qed.
+Proof. exact: lteif_subl_addl. Qed.
 
 Lemma lersif_subr_addl b x y z : (x <= y - z ?< if b) = (z + x <= y ?< if b).
-Proof. by case: b; apply lter_sub_addl. Qed.
+Proof. exact: lteif_subr_addl. Qed.
 
 Definition lersif_sub_addl := (lersif_subl_addl, lersif_subr_addl).
 
-Lemma lersif_andb x y : {morph lersif x y : p q / p || q >-> p && q}.
-Proof.
-by case=> [] [] /=; rewrite ?le_eqVlt;
-  case: (_ < _)%R; rewrite ?(orbT, orbF, andbF, andbb).
-Qed.
+Lemma lersif_andb x y :
+  {morph (fun b => lersif x y b) : p q / p || q >-> p && q}.
+Proof. by move=> ? ?; rewrite negb_or lteif_andb. Qed.
 
-Lemma lersif_orb x y : {morph lersif x y : p q / p && q >-> p || q}.
-Proof.
-by case=> [] [] /=; rewrite ?le_eqVlt;
-  case: (_ < _)%R; rewrite ?(orbT, orbF, orbb).
-Qed.
+Lemma lersif_orb x y :
+  {morph (fun b => lersif x y b) : p q / p && q >-> p || q}.
+Proof. by move=> ? ?; rewrite negb_and lteif_orb. Qed.
 
-Lemma lersif_imply b1 b2 r1 r2 :
+Lemma lersif_imply b1 b2 (r1 r2 : R) :
   b2 ==> b1 -> r1 <= r2 ?< if b1 -> r1 <= r2 ?< if b2.
-Proof. by case: b1 b2 => [] [] //= _ /ltW. Qed.
+Proof. by move=> ?; apply: lteif_imply; rewrite implybNN. Qed.
 
 Lemma lersifW b x y : x <= y ?< if b -> x <= y.
-Proof. by case: b => // /ltW. Qed.
+Proof. exact: lteifW. Qed.
 
 Lemma ltrW_lersif b x y : x < y -> x <= y ?< if b.
-Proof. by case: b => // /ltW. Qed.
+Proof. exact: ltrW_lteif. Qed.
 
 Lemma lersif_pmul2l b x : 0 < x -> {mono *%R x : y z / y <= z ?< if b}.
-Proof. by case: b; apply lter_pmul2l. Qed.
+Proof. exact: lteif_pmul2l. Qed.
 
 Lemma lersif_pmul2r b x : 0 < x -> {mono *%R^~ x : y z / y <= z ?< if b}.
-Proof. by case: b; apply lter_pmul2r. Qed.
+Proof. exact: lteif_pmul2r. Qed.
 
 Lemma lersif_nmul2l b x : x < 0 -> {mono *%R x : y z /~ y <= z ?< if b}.
-Proof. by case: b; apply lter_nmul2l. Qed.
+Proof. exact: lteif_nmul2l. Qed.
 
 Lemma lersif_nmul2r b x : x < 0 -> {mono *%R^~ x : y z /~ y <= z ?< if b}.
-Proof. by case: b; apply lter_nmul2r. Qed.
+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. by case: b => [] xR yR /=; case: real_ltgtP. Qed.
+Proof. exact: real_lteifNE. Qed.
 
 Lemma real_lersif_norml b x y :
   x \is Num.real ->
   (`|x| <= y ?< if b) = ((- y <= x ?< if b) && (x <= y ?< if b)).
-Proof. by case: b; apply real_lter_norml. Qed.
+Proof. exact: real_lteif_norml. Qed.
 
 Lemma real_lersif_normr b x y :
   y \is Num.real ->
   (x <= `|y| ?< if b) = ((x <= y ?< if b) || (x <= - y ?< if b)).
-Proof. by case: b; apply real_lter_normr. Qed.
+Proof. exact: real_lteif_normr. Qed.
 
 Lemma lersif_nnormr b x y : y <= 0 ?< if ~~ b -> (`|x| <= y ?< if b) = false.
-Proof. by case: b => /=; apply lter_nnormr. Qed.
+Proof. exact: lteif_nnormr. Qed.
 
 End LersifPo.
 
-Notation "x <= y ?< 'if' b" := (lersif x y b)
-  (at level 70, y at next level,
-  format "x '[hv'  <=  y '/'  ?<  'if'  b ']'") : ring_scope.
-
 Section LersifOrdered.
 
 Variable (R : realDomainType) (b : bool) (x y z e : R).
 
 Lemma lersifN : (x <= y ?< if ~~ b) = ~~ (y <= x ?< if b).
-Proof. by rewrite real_lersifN ?num_real. Qed.
+Proof. exact: lteifNE. Qed.
 
 Lemma lersif_norml :
   (`|x| <= y ?< if b) = (- y <= x ?< if b) && (x <= y ?< if b).
-Proof. by case: b; apply lter_norml. Qed.
+Proof. exact: lteif_norml. Qed.
 
 Lemma lersif_normr :
   (x <= `|y| ?< if b) = (x <= y ?< if b) || (x <= - y ?< if b).
-Proof. by case: b; apply lter_normr. Qed.
+Proof. exact: lteif_normr. Qed.
 
 Lemma lersif_distl :
   (`|x - y| <= e ?< if b) = (y - e <= x ?< if b) && (x <= y + e ?< if b).
-Proof. by case: b; apply lter_distl. Qed.
+Proof. exact: lteif_distl. Qed.
 
 Lemma lersif_minr :
   (x <= Num.min y z ?< if b) = (x <= y ?< if b) && (x <= z ?< if b).
-Proof. by case: b; rewrite /= (le_minr, lt_minr). Qed.
+Proof. exact: lteif_minr. Qed.
 
 Lemma lersif_minl :
   (Num.min y z <= x ?< if b) = (y <= x ?< if b) || (z <= x ?< if b).
-Proof. by case: b; rewrite /= (le_minl, lt_minl). Qed.
+Proof. exact: lteif_minl. Qed.
 
 Lemma lersif_maxr :
   (x <= Num.max y z ?< if b) = (x <= y ?< if b) || (x <= z ?< if b).
-Proof. by case: b; rewrite /= (le_maxr, lt_maxr). Qed.
+Proof. exact: lteif_maxr. Qed.
 
 Lemma lersif_maxl :
   (Num.max y z <= x ?< if b) = (y <= x ?< if b) && (z <= x ?< if b).
-Proof. by case: b; rewrite /= (le_maxl, lt_maxl). Qed.
+Proof. exact: lteif_maxl. Qed.
 
 End LersifOrdered.
 
@@ -231,406 +811,501 @@ Section LersifField.
 Variable (F : numFieldType) (b : bool) (z x y : F).
 
 Lemma lersif_pdivl_mulr : 0 < z -> x <= y / z ?< if b = (x * z <= y ?< if b).
-Proof. by case: b => ? /=; rewrite lter_pdivl_mulr. Qed.
+Proof. exact: lteif_pdivl_mulr. Qed.
 
 Lemma lersif_pdivr_mulr : 0 < z -> y / z <= x ?< if b = (y <= x * z ?< if b).
-Proof. by case: b => ? /=; rewrite lter_pdivr_mulr. Qed.
+Proof. exact: lteif_pdivr_mulr. Qed.
 
 Lemma lersif_pdivl_mull : 0 < z -> x <= z^-1 * y ?< if b = (z * x <= y ?< if b).
-Proof. by case: b => ? /=; rewrite lter_pdivl_mull. Qed.
+Proof. exact: lteif_pdivl_mull. Qed.
 
 Lemma lersif_pdivr_mull : 0 < z -> z^-1 * y <= x ?< if b = (y <= z * x ?< if b).
-Proof. by case: b => ? /=; rewrite lter_pdivr_mull. Qed.
+Proof. exact: lteif_pdivr_mull. Qed.
 
 Lemma lersif_ndivl_mulr : z < 0 -> x <= y / z ?< if b = (y <= x * z ?< if b).
-Proof. by case: b => ? /=; rewrite lter_ndivl_mulr. Qed.
+Proof. exact: lteif_ndivl_mulr. Qed.
 
 Lemma lersif_ndivr_mulr : z < 0 -> y / z <= x ?< if b = (x * z <= y ?< if b).
-Proof. by case: b => ? /=; rewrite lter_ndivr_mulr. Qed.
+Proof. exact: lteif_ndivr_mulr. Qed.
 
 Lemma lersif_ndivl_mull : z < 0 -> x <= z^-1 * y ?< if b = (y <=z * x ?< if b).
-Proof. by case: b => ? /=; rewrite lter_ndivl_mull. Qed.
+Proof. exact: lteif_ndivl_mull. Qed.
 
 Lemma lersif_ndivr_mull : z < 0 -> z^-1 * y <= x ?< if b = (z * x <= y ?< if b).
-Proof. by case: b => ? /=; rewrite lter_ndivr_mull. Qed.
+Proof. exact: lteif_ndivr_mull. Qed.
 
 End LersifField.
 
-Variant itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
-Notation BOpen := (BOpen_if true).
-Notation BClose := (BOpen_if false).
-Variant interval (T : Type) := Interval of itv_bound T & itv_bound T.
+Section IntervalPo.
 
-(* We provide the 9 following notations to help writing formal intervals *)
-Notation "`[ a , b ]" := (Interval (BClose a) (BClose b))
-  (at level 0, a, b at level 9 , format "`[ a ,  b ]") : ring_scope.
-Notation "`] a , b ]" := (Interval (BOpen a) (BClose b))
-  (at level 0, a, b at level 9 , format "`] a ,  b ]") : ring_scope.
-Notation "`[ a , b [" := (Interval (BClose a) (BOpen b))
-  (at level 0, a, b at level 9 , format "`[ a ,  b [") : ring_scope.
-Notation "`] a , b [" := (Interval (BOpen a) (BOpen b))
-  (at level 0, a, b at level 9 , format "`] a ,  b [") : ring_scope.
-Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b))
-  (at level 0, b at level 9 , format "`] '-oo' ,  b ]") : ring_scope.
-Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b))
-  (at level 0, b at level 9 , format "`] '-oo' ,  b [") : ring_scope.
-Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _))
-  (at level 0, a at level 9 , format "`[ a ,  '+oo' [") : ring_scope.
-Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _))
-  (at level 0, a at level 9 , format "`] a ,  '+oo' [") : ring_scope.
-Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _))
-  (at level 0, format "`] -oo ,  '+oo' [") : ring_scope.
+Variable R : numDomainType.
 
-Section IntervalEq.
+Implicit Types (x xa xb : R).
 
-Variable T : eqType.
+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.
 
-Definition eq_itv_bound (b1 b2 : itv_bound T) : bool :=
-  match b1, b2 with
-    | BOpen_if a x, BOpen_if b y => (a == b) && (x == y)
-    | BInfty, BInfty => true
-    | _, _ => false
-  end.
+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 eq_itv_boundP : Equality.axiom eq_itv_bound.
-Proof.
-move=> b1 b2; apply: (iffP idP).
-- by move: b1 b2 => [a x |] [b y |] => //= /andP [] /eqP -> /eqP ->.
-- by move=> <-; case: b1 => //= a x; rewrite !eqxx.
-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.
 
-Canonical itv_bound_eqMixin := EqMixin eq_itv_boundP.
-Canonical itv_bound_eqType :=
-  Eval hnf in EqType (itv_bound T) itv_bound_eqMixin.
+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.
 
-Definition eqitv (x y : interval T) : bool :=
-  let: Interval x x' := x in
-  let: Interval y y' := y in (x == y) && (x' == y').
+End IntervalPo.
 
-Lemma eqitvP : Equality.axiom eqitv.
-Proof.
-move=> x y; apply: (iffP idP).
-- by move: x y => [x x'] [y y'] => //= /andP [] /eqP -> /eqP ->.
-- by move=> <-; case: x => /= x x'; rewrite !eqxx.
-Qed.
+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.
 
-Canonical interval_eqMixin := EqMixin eqitvP.
-Canonical interval_eqType := Eval hnf in EqType (interval T) interval_eqMixin.
+End mc_1_11.
 
-End IntervalEq.
+(* Use `Order.lteif` instead of `lteif`. (`deprecate` does not accept a       *)
+(* qualified name.)                                                           *)
+Local Notation lteif := Order.lteif (only parsing).
 
-Section IntervalPo.
+Notation "@ 'lersif'" :=
+  ((fun _ (R : numDomainType) x y b => @Order.lteif _ R x y (~~ b))
+     (deprecate lersif lteif))
+    (at level 10, only parsing).
 
-Variable R : numDomainType.
+Notation lersif := (@lersif _) (only parsing).
 
-Definition pred_of_itv (i : interval R) : pred R :=
-  [pred x | let: Interval l u := i in
-      match l with
-        | BOpen_if b lb => lb <= x ?< if b
-        | BInfty => true
-      end &&
-      match u with
-        | BOpen_if b ub => x <= ub ?< if b
-        | BInfty => true
-      end].
-Canonical Structure itvPredType := PredType pred_of_itv.
+Notation "x <= y ?< 'if' b" :=
+  ((fun _ => x < y ?<= if ~~ b) (deprecate lersif lteif))
+    (at level 70, y at next level, only parsing) : ring_scope.
 
-(* we compute a set of rewrite rules associated to an interval *)
-Definition itv_rewrite (i : interval R) x : Type :=
-  let: Interval l u := i in
-    (match l with
-       | BClose a => (a <= x) * (x < a = false)
-       | BOpen a => (a <= x) * (a < x) * (x <= a = false) * (x < a = false)
-       | BInfty => forall x : R, x == x
-     end *
-    match u with
-       | BClose b => (x <= b) * (b < x = false)
-       | BOpen b => (x <= b) * (x < b) * (b <= x = false) * (b < x = false)
-       | BInfty => forall x : R, x == x
-     end *
-    match l, u with
-       | BClose a, BClose b =>
-         (a <= b) * (b < a = false) * (a \in `[a, b]) * (b \in `[a, b])
-       | BClose a, BOpen b =>
-         (a <= b) * (a < b) * (b <= a = false) * (b < a = false)
-         * (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b])
-       | BOpen a, BClose b =>
-         (a <= b) * (a < b) * (b <= a = false) * (b < a = false)
-         * (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b])
-       | BOpen a, BOpen b =>
-         (a <= b) * (a < b) * (b <= a = false) * (b < a = false)
-         * (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b])
-       | _, _ => forall x : R, x == x
-    end)%type.
+(* LersifPo *)
 
-Definition itv_decompose (i : interval R) x : Prop :=
-  let: Interval l u := i in
-  ((match l with
-    | BOpen_if b lb => (lb <= x ?< if b) : Prop
-    | BInfty => True
-  end : Prop) *
-  (match u with
-    | BOpen_if b ub => (x <= ub ?< if b) : Prop
-    | BInfty => True
-  end : Prop))%type.
-
-Lemma itv_dec : forall (x : R) (i : interval R),
-  reflect (itv_decompose i x) (x \in i).
-Proof. by move=> ? [[? ?|] [? ?|]]; apply: (iffP andP); case. Qed.
+Notation "@ 'subr_lersifr0'" :=
+  ((fun _ => @mc_1_11.subr_lersifr0) (deprecate subr_lersifr0 subr_lteifr0))
+    (at level 10, only parsing).
 
-Arguments itv_dec {x i}.
+Notation subr_lersifr0 := (@subr_lersifr0 _) (only parsing).
 
-Definition le_boundl (b1 b2 : itv_bound R) :=
-  match b1, b2 with
-    | BOpen_if b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if ~~ b2 && b1
-    | BOpen_if _ _, BInfty => false
-    | _, _ => true
-  end.
+Notation "@ 'subr_lersif0r'" :=
+  ((fun _ => @mc_1_11.subr_lersif0r) (deprecate subr_lersif0r subr_lteif0r))
+    (at level 10, only parsing).
 
-Definition le_boundr (b1 b2 : itv_bound R) :=
-  match b1, b2 with
-    | BOpen_if b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if ~~ b1 && b2
-    | BInfty, BOpen_if _ _ => false
-    | _, _ => true
-  end.
+Notation subr_lersif0r := (@subr_lersif0r _) (only parsing).
 
-Lemma itv_boundlr bl br x :
-  (x \in Interval bl br) =
-  (le_boundl bl (BClose x)) && (le_boundr (BClose x) br).
-Proof. by case: bl br => [? ? |] []. Qed.
+Notation subr_lersif0 :=
+  ((fun _ => @mc_1_11.subr_lersif0) (deprecate subr_lersif0 subr_lteif0))
+    (only parsing).
 
-Lemma le_boundl_refl : reflexive le_boundl.
-Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed.
+Notation "@ 'lersif_trans'" :=
+  ((fun _ => @mc_1_11.lersif_trans) (deprecate lersif_trans lteif_trans))
+    (at level 10, only parsing).
 
-Hint Resolve le_boundl_refl : core.
+Notation lersif_trans := (@lersif_trans _ _ _ _ _ _) (only parsing).
 
-Lemma le_boundr_refl : reflexive le_boundr.
-Proof. by move=> [[] b|]; rewrite /le_boundr /= ?lerr. Qed.
+Notation lersif01 :=
+  ((fun _ => @mc_1_11.lersif01) (deprecate lersif01 lteif01)) (only parsing).
 
-Hint Resolve le_boundr_refl : core.
+Notation "@ 'lersif_anti'" :=
+  ((fun _ => @mc_1_11.lersif_anti) (deprecate lersif_anti lteif_anti))
+    (at level 10, only parsing).
 
-Lemma le_boundl_trans : transitive le_boundl.
-Proof.
-by move=> [[] x|] [[] y|] [[] z|] lexy leyz //;
-  apply: (lersif_imply _ (lersif_trans lexy leyz)).
-Qed.
+Notation lersif_anti := (@lersif_anti _) (only parsing).
 
-Lemma le_boundr_trans : transitive le_boundr.
-Proof.
-by move=> [[] x|] [[] y|] [[] z|] lexy leyz //;
-  apply: (lersif_imply _ (lersif_trans lexy leyz)).
-Qed.
+Notation "@ 'lersifxx'" :=
+  ((fun _ => @mc_1_11.lersifxx) (deprecate lersifxx lteifxx))
+    (at level 10, only parsing).
 
-Lemma le_boundl_bb x b1 b2 :
-  le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).
-Proof. by rewrite /le_boundl lersifxx andbC negb_and negbK implybE. Qed.
+Notation lersifxx := (@lersifxx _) (only parsing).
 
-Lemma le_boundr_bb x b1 b2 :
-  le_boundr (BOpen_if b1 x) (BOpen_if b2 x) = (b2 ==> b1).
-Proof. by rewrite /le_boundr lersifxx andbC negb_and negbK implybE. Qed.
+Notation "@ 'lersifNF'" :=
+  ((fun _ => @mc_1_11.lersifNF) (deprecate lersifNF lteifNF))
+    (at level 10, only parsing).
 
-Lemma le_boundl_anti b1 b2 : (le_boundl b1 b2 && le_boundl b2 b1) = (b1 == b2).
-Proof. by case: b1 b2 => [[] lr1 |] [[] lr2 |] //; rewrite lersif_anti. Qed.
+Notation lersifNF := (@lersifNF _ _ _ _) (only parsing).
 
-Lemma le_boundr_anti b1 b2 : (le_boundr b1 b2 && le_boundr b2 b1) = (b1 == b2).
-Proof. by case: b1 b2 => [[] lr1 |] [[] lr2 |] //; rewrite lersif_anti. Qed.
+Notation "@ 'lersifS'" :=
+  ((fun _ => @mc_1_11.lersifS) (deprecate lersifS lteifS))
+    (at level 10, only parsing).
 
-Lemma itv_xx x bl br :
-  Interval (BOpen_if bl x) (BOpen_if br x) =i 
-  if ~~ (bl || br) then pred1 x else pred0.
-Proof. by move: bl br => [] [] y /=; rewrite !inE lersif_anti. Qed.
+Notation lersifS := (@lersifS _ _ _) (only parsing).
 
-Lemma itv_gte ba xa bb xb :  xb <= xa ?< if ~~ (ba || bb) 
-  -> Interval (BOpen_if ba xa) (BOpen_if bb xb) =i pred0.
-Proof.
-move=> ? y; rewrite itv_boundlr inE /=.
-by apply/negP => /andP [] lexay /(lersif_trans lexay); rewrite lersifNF.
-Qed.
+Notation "@ 'lersifT'" :=
+  ((fun _ => @mc_1_11.lersifT) (deprecate lersifT lteifT))
+    (at level 10, only parsing).
 
-Lemma boundl_in_itv : forall ba xa b,
-  xa \in Interval (BOpen_if ba xa) b = 
-  if ba then false else le_boundr (BClose xa) b.
-Proof. by move=> [] xa [b xb|]; rewrite inE lersifxx. Qed.
+Notation lersifT := (@lersifT _) (only parsing).
 
-Lemma boundr_in_itv : forall bb xb a,
-  xb \in Interval a (BOpen_if bb xb) =
-  if bb then false else le_boundl a (BClose xb).
-Proof. by move=> [] xb [b xa|]; rewrite inE lersifxx /= ?andbT ?andbF. Qed.
+Notation "@ 'lersifF'" :=
+  ((fun _ => @mc_1_11.lersifF) (deprecate lersifF lteifF))
+    (at level 10, only parsing).
 
-Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
+Notation lersifF := (@lersifF _) (only parsing).
 
-Lemma itvP : forall (x : R) (i : interval R), x \in i -> itv_rewrite i x.
-Proof.
-move=> x [[[] a|] [[] b|]] /itv_dec [ha hb]; do !split;
-  rewrite ?bound_in_itv //=; do 1?[apply/negbTE; rewrite (le_gtF, lt_geF)];
-  by [ | apply: ltW | move: (lersif_trans ha hb) => //=; exact: ltW ].
-Qed.
+Notation "@ 'lersif_oppl'" :=
+  ((fun _ => @mc_1_11.lersif_oppl) (deprecate lersif_oppl lteif_oppl))
+    (at level 10, only parsing).
 
-Arguments itvP [x i].
+Notation lersif_oppl := (@lersif_oppl _) (only parsing).
 
-Definition itv_intersection (x y : interval R) : interval R :=
-  let: Interval x x' := x in
-  let: Interval y y' := y in
-  Interval
-    (if le_boundl x y then y else x)
-    (if le_boundr x' y' then x' else y').
+Notation "@ 'lersif_oppr'" :=
+  ((fun _ => @mc_1_11.lersif_oppr) (deprecate lersif_oppr lteif_oppr))
+    (at level 10, only parsing).
 
-Definition itv_intersection1i : left_id `]-oo, +oo[ itv_intersection.
-Proof. by case=> i []. Qed.
+Notation lersif_oppr := (@lersif_oppr _) (only parsing).
 
-Definition itv_intersectioni1 : right_id `]-oo, +oo[ itv_intersection.
-Proof. by case=> [[lb lr |] [ub ur |]]. Qed.
+Notation "@ 'lersif_0oppr'" :=
+  ((fun _ => @mc_1_11.lersif_0oppr) (deprecate lersif_0oppr lteif_0oppr))
+    (at level 10, only parsing).
 
-Lemma itv_intersectionii : idempotent itv_intersection.
-Proof. by case=> [[[] lr |] [[] ur |]] //=; rewrite !lexx. Qed.
+Notation lersif_0oppr := (@lersif_0oppr _) (only parsing).
 
-Definition subitv (i1 i2 : interval R) :=
-  match i1, i2 with
-    | Interval a1 b1, Interval a2 b2 => le_boundl a2 a1 && le_boundr b1 b2
-  end.
+Notation "@ 'lersif_oppr0'" :=
+  ((fun _ => @mc_1_11.lersif_oppr0) (deprecate lersif_oppr0 lteif_oppr0))
+    (at level 10, only parsing).
 
-Lemma subitvP : forall (i2 i1 : interval R), subitv i1 i2 -> {subset i1 <= i2}.
-Proof.
-by move=> [[b2 l2|] [b2' u2|]] [[b1 l1|] [b1' u1|]]
-          /andP [] /= ha hb x /andP [ha' hb']; apply/andP; split => //;
-  (apply/lersif_imply: (lersif_trans ha ha'); case: b1 b2 ha ha' => [] []) ||
-  (apply/lersif_imply: (lersif_trans hb' hb); case: b1' b2' hb hb' => [] []).
-Qed.
+Notation lersif_oppr0 := (@lersif_oppr0 _) (only parsing).
 
-Lemma subitvPr (a b1 b2 : itv_bound R) :
-  le_boundr b1 b2 -> {subset (Interval a b1) <= (Interval a b2)}.
-Proof. by move=> leb; apply: subitvP; rewrite /= leb andbT. Qed.
+Notation "@ 'lersif_opp2'" :=
+  ((fun _ => @mc_1_11.lersif_opp2) (deprecate lersif_opp2 lteif_opp2))
+    (at level 10, only parsing).
 
-Lemma subitvPl (a1 a2 b : itv_bound R) :
-  le_boundl a2 a1 -> {subset (Interval a1 b) <= (Interval a2 b)}.
-Proof. by move=> lea; apply: subitvP; rewrite /= lea /=. Qed.
+Notation lersif_opp2 := (@lersif_opp2 _) (only parsing).
 
-Lemma lersif_in_itv ba bb xa xb x :
-  x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) ->
-        xa <= xb ?< if ba || bb.
-Proof. by case: ba bb => [] [] /itvP /= ->. Qed.
+Notation lersif_oppE :=
+  ((fun _ => @mc_1_11.lersif_oppE) (deprecate lersif_oppE lteif_oppE))
+    (only parsing).
 
-Lemma ltr_in_itv ba bb xa xb x :
-  ba || bb -> x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> xa < xb.
-Proof. by move=> bab /lersif_in_itv; rewrite bab. Qed.
+Notation "@ 'lersif_add2l'" :=
+  ((fun _ => @mc_1_11.lersif_add2l) (deprecate lersif_add2l lteif_add2l))
+    (at level 10, only parsing).
 
-Lemma ler_in_itv ba bb xa xb x :
-  x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> xa <= xb.
-Proof. by move/lersif_in_itv/lersifW. Qed.
+Notation lersif_add2l := (@lersif_add2l _) (only parsing).
 
-Lemma mem0_itvcc_xNx x : (0 \in `[-x, x]) = (0 <= x).
-Proof. by rewrite !inE /= oppr_le0 andbb. Qed.
+Notation "@ 'lersif_add2r'" :=
+  ((fun _ => @mc_1_11.lersif_add2r) (deprecate lersif_add2r lteif_add2r))
+    (at level 10, only parsing).
 
-Lemma mem0_itvoo_xNx x : 0 \in `](-x), x[ = (0 < x).
-Proof. by rewrite !inE /= oppr_lt0 andbb. Qed.
+Notation lersif_add2r := (@lersif_add2r _) (only parsing).
 
-Lemma itv_splitI : forall a b x,
-  x \in Interval a b =
-  (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b).
-Proof. by move=> [? ?|] [? ?|] ?; rewrite !inE ?andbT. Qed.
+Notation lersif_add2 :=
+  ((fun _ => @mc_1_11.lersif_add2) (deprecate lersif_add2 lteif_add2))
+    (only parsing).
 
-Lemma oppr_itv ba bb (xa xb x : R) :
-  (-x \in Interval (BOpen_if ba xa) (BOpen_if bb xb)) = 
-  (x \in Interval (BOpen_if bb (-xb)) (BOpen_if ba (-xa))).
-Proof. by rewrite !inE lersif_oppr andbC lersif_oppl. Qed.
+Notation "@ 'lersif_subl_addr'" :=
+  ((fun _ => @mc_1_11.lersif_subl_addr)
+     (deprecate lersif_subl_addr lteif_subl_addr))
+    (at level 10, only parsing).
 
-Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[).
-Proof. exact: oppr_itv. Qed.
+Notation lersif_subl_addr := (@lersif_subl_addr _) (only parsing).
 
-Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]).
-Proof. exact: oppr_itv. Qed.
+Notation "@ 'lersif_subr_addr'" :=
+  ((fun _ => @mc_1_11.lersif_subr_addr)
+     (deprecate lersif_subr_addr lteif_subr_addr))
+    (at level 10, only parsing).
 
-Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[).
-Proof. exact: oppr_itv. Qed.
+Notation lersif_subr_addr := (@lersif_subr_addr _) (only parsing).
 
-Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]).
-Proof. exact: oppr_itv. Qed.
+Notation lersif_sub_addr :=
+  ((fun _ => @mc_1_11.lersif_sub_addr)
+     (deprecate lersif_sub_addr lteif_sub_addr))
+    (only parsing).
 
-End IntervalPo.
+Notation "@ 'lersif_subl_addl'" :=
+  ((fun _ => @mc_1_11.lersif_subl_addl)
+     (deprecate lersif_subl_addl lteif_subl_addl))
+    (at level 10, only parsing).
 
-Section IntervalOrdered.
+Notation lersif_subl_addl := (@lersif_subl_addl _) (only parsing).
 
-Variable R : realDomainType.
+Notation "@ 'lersif_subr_addl'" :=
+  ((fun _ => @mc_1_11.lersif_subr_addl)
+     (deprecate lersif_subr_addl lteif_subr_addl))
+    (at level 10, only parsing).
 
-Lemma le_boundl_total : total (@le_boundl R).
-Proof. by move=> [[] l |] [[] r |] //=; case: (ltrgtP l r). Qed.
+Notation lersif_subr_addl := (@lersif_subr_addl _) (only parsing).
 
-Lemma le_boundr_total : total (@le_boundr R).
-Proof. by move=> [[] l |] [[] r |] //=; case: (ltrgtP l r). Qed.
+Notation lersif_sub_addl :=
+  ((fun _ => @mc_1_11.lersif_sub_addl)
+     (deprecate lersif_sub_addl lteif_sub_addl))
+    (only parsing).
 
-Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b ->
-  forall y, y \in Interval a b =
-    (y \in Interval a (BOpen_if (~~ bc) xc))
-    || (y \in Interval (BOpen_if bc xc) b).
-Proof.
-move=> xc_in y; move: xc_in.
-rewrite !itv_boundlr [le_boundr (BClose _) (BOpen_if _ _)]/=
-        [le_boundr]lock /= lersifN -lock.
-case/andP => leaxc lexcb;
-  case: (boolP (le_boundl a _)) => leay; case: (boolP (le_boundr _ b)) => leyb;
-  rewrite /= (andbT, andbF) ?orbF ?orNb //=;
-  [apply/esym/negbF | apply/esym/negbTE].
-- by case: b lexcb leyb => //= bb b; rewrite -lersifN => lexcb leyb;
-    apply/lersif_imply: (lersif_trans lexcb leyb); rewrite orbN implybT.
-- by case: a leaxc leay => //= ab a leaxc;
-    apply/contra => /(lersif_trans leaxc);
-    apply/lersif_imply; rewrite implybE orbA orNb.
-Qed.
+Notation "@ 'lersif_andb'" :=
+  ((fun _ => @mc_1_11.lersif_andb) (deprecate lersif_andb lteif_andb))
+    (at level 10, only parsing).
 
-Lemma itv_splitU2 (x : R) a b : x \in Interval a b ->
-  forall y, y \in Interval a b =
-    [|| (y \in Interval a (BOpen x)), (y == x)
-      | (y \in Interval (BOpen 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 [].
-Qed.
+Notation lersif_andb := (@lersif_andb _) (only parsing).
 
-Lemma itv_intersectionC : commutative (@itv_intersection R).
-Proof.
-move=> [x x'] [y y'] /=; congr Interval; do 2 case: ifP => //=.
-- by move=> leyx lexy; apply/eqP; rewrite -le_boundl_anti leyx lexy.
-- by case/orP: (le_boundl_total x y) => ->.
-- by move=> leyx' lexy'; apply/eqP; rewrite -le_boundr_anti leyx' lexy'.
-- by case/orP: (le_boundr_total x' y') => ->.
-Qed.
+Notation "@ 'lersif_orb'" :=
+  ((fun _ => @mc_1_11.lersif_orb) (deprecate lersif_orb lteif_orb))
+    (at level 10, only parsing).
 
-Lemma itv_intersectionA : associative (@itv_intersection R).
-Proof.
-move=> [x x'] [y y'] [z z'] /=; congr Interval;
-  do !case: ifP => //=; do 1?congruence.
-- by move=> lexy leyz; rewrite (le_boundl_trans lexy leyz).
-- move=> gtxy lexz gtyz _; apply/eqP; rewrite -le_boundl_anti lexz /=.
-  move: (le_boundl_total y z) (le_boundl_total x y).
-  by rewrite gtxy gtyz; apply: le_boundl_trans.
-- by move=> lexy' gtxz' leyz'; rewrite (le_boundr_trans lexy' leyz') in gtxz'.
-- move=> gtxy' gtyz' _ lexz'; apply/eqP; rewrite -le_boundr_anti lexz' /=.
-  move: (le_boundr_total y' z') (le_boundr_total x' y').
-  by rewrite gtxy' gtyz'; apply: le_boundr_trans.
-Qed.
+Notation lersif_orb := (@lersif_orb _) (only parsing).
 
-Canonical itv_intersection_monoid :=
-  Monoid.Law itv_intersectionA (@itv_intersection1i R) (@itv_intersectioni1 R).
+Notation "@ 'lersif_imply'" :=
+  ((fun _ => @mc_1_11.lersif_imply) (deprecate lersif_imply lteif_imply))
+    (at level 10, only parsing).
 
-Canonical itv_intersection_comoid := Monoid.ComLaw itv_intersectionC.
+Notation lersif_imply := (@lersif_imply _ _ _ _ _) (only parsing).
 
-End IntervalOrdered.
+Notation "@ 'lersifW'" :=
+  ((fun _ => @mc_1_11.lersifW) (deprecate lersifW lteifW))
+    (at level 10, only parsing).
 
-Section IntervalField.
+Notation lersifW := (@lersifW _ _ _ _) (only parsing).
 
-Variable R : realFieldType.
+Notation "@ 'ltrW_lersif'" :=
+  ((fun _ => @mc_1_11.ltrW_lersif) (deprecate ltrW_lersif ltrW_lteif))
+    (at level 10, only parsing).
 
-Lemma mid_in_itv : forall ba bb (xa xb : R), xa <= xb ?< if ba || bb
-  -> mid xa xb \in Interval (BOpen_if ba xa) (BOpen_if bb xb).
-Proof.
-by move=> [] [] xa xb /= ?; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltW.
-Qed.
+Notation ltrW_lersif := (@ltrW_lersif _) (only parsing).
 
-Lemma mid_in_itvoo : forall (xa xb : R), xa < xb -> mid xa xb \in `]xa, xb[.
-Proof. by move=> xa xb ?; apply: mid_in_itv. Qed.
+Notation "@ 'lersif_pmul2l'" :=
+  ((fun _ => @mc_1_11.lersif_pmul2l) (deprecate lersif_pmul2l lteif_pmul2l))
+    (at level 10, only parsing).
 
-Lemma mid_in_itvcc : forall (xa xb : R), xa <= xb -> mid xa xb \in `[xa, xb].
-Proof. by move=> xa xb ?; apply: mid_in_itv. Qed.
+Notation lersif_pmul2l := (fun b => @lersif_pmul2l _ b _) (only parsing).
 
-End IntervalField.
+Notation "@ 'lersif_pmul2r'" :=
+  ((fun _ => @mc_1_11.lersif_pmul2r) (deprecate lersif_pmul2r lteif_pmul2r))
+    (at level 10, only parsing).
+
+Notation lersif_pmul2r := (fun b => @lersif_pmul2r _ b _) (only parsing).
+
+Notation "@ 'lersif_nmul2l'" :=
+  ((fun _ => @mc_1_11.lersif_nmul2l) (deprecate lersif_nmul2l lteif_nmul2l))
+    (at level 10, only parsing).
+
+Notation lersif_nmul2l := (fun b => @lersif_nmul2l _ b _) (only parsing).
+
+Notation "@ 'lersif_nmul2r'" :=
+  ((fun _ => @mc_1_11.lersif_nmul2r) (deprecate lersif_nmul2r lteif_nmul2r))
+    (at level 10, only parsing).
+
+Notation lersif_nmul2r := (fun b => @lersif_nmul2r _ b _) (only parsing).
+
+Notation "@ 'real_lersifN'" :=
+  ((fun _ => @mc_1_11.real_lersifN) (deprecate real_lersifN real_lteifNE))
+    (at level 10, only parsing).
+
+Notation real_lersifN := (@real_lersifN _ _ _) (only parsing).
+
+Notation "@ 'real_lersif_norml'" :=
+  ((fun _ => @mc_1_11.real_lersif_norml)
+     (deprecate real_lersif_norml real_lteif_norml))
+    (at level 10, only parsing).
+
+Notation real_lersif_norml :=
+  (fun b => @real_lersif_norml _ b _) (only parsing).
+
+Notation "@ 'real_lersif_normr'" :=
+  ((fun _ => @mc_1_11.real_lersif_normr)
+     (deprecate real_lersif_normr real_lteif_normr))
+    (at level 10, only parsing).
+
+Notation real_lersif_normr :=
+  (fun b x => @real_lersif_normr _ b x _) (only parsing).
+
+Notation "@ 'lersif_nnormr'" :=
+  ((fun _ => @mc_1_11.lersif_nnormr) (deprecate lersif_nnormr lteif_nnormr))
+    (at level 10, only parsing).
+
+Notation lersif_nnormr := (fun x => @lersif_nnormr _ _ x _) (only parsing).
+
+(* LersifOrdered *)
+
+Notation "@ 'lersifN'" :=
+  ((fun _ => @mc_1_11.lersifN) (deprecate lersifN lteifNE))
+    (at level 10, only parsing).
+
+Notation lersifN := (@lersifN _) (only parsing).
+
+Notation "@ 'lersif_norml'" :=
+  ((fun _ => @mc_1_11.lersif_norml) (deprecate lersif_norml lteif_norml))
+    (at level 10, only parsing).
+
+Notation lersif_norml := (@lersif_norml _) (only parsing).
+
+Notation "@ 'lersif_normr'" :=
+  ((fun _ => @mc_1_11.lersif_normr) (deprecate lersif_normr lteif_normr))
+    (at level 10, only parsing).
+
+Notation lersif_normr := (@lersif_normr _) (only parsing).
+
+Notation "@ 'lersif_distl'" :=
+  ((fun _ => @mc_1_11.lersif_distl) (deprecate lersif_distl lteif_distl))
+    (at level 10, only parsing).
+
+Notation lersif_distl := (@lersif_distl _) (only parsing).
+
+Notation "@ 'lersif_minr'" :=
+  ((fun _ => @mc_1_11.lersif_minr) (deprecate lersif_minr lteif_minr))
+    (at level 10, only parsing).
+
+Notation lersif_minr := (@lersif_minr _) (only parsing).
+
+Notation "@ 'lersif_minl'" :=
+  ((fun _ => @mc_1_11.lersif_minl) (deprecate lersif_minl lteif_minl))
+    (at level 10, only parsing).
+
+Notation lersif_minl := (@lersif_minl _) (only parsing).
+
+Notation "@ 'lersif_maxr'" :=
+  ((fun _ => @mc_1_11.lersif_maxr) (deprecate lersif_maxr lteif_maxr))
+    (at level 10, only parsing).
+
+Notation lersif_maxr := (@lersif_maxr _) (only parsing).
+
+Notation "@ 'lersif_maxl'" :=
+  ((fun _ => @mc_1_11.lersif_maxl) (deprecate lersif_maxl lteif_maxl))
+    (at level 10, only parsing).
+
+Notation lersif_maxl := (@lersif_maxl _) (only parsing).
+
+(* LersifField *)
+
+Notation "@ 'lersif_pdivl_mulr'" :=
+  ((fun _ => @mc_1_11.lersif_pdivl_mulr)
+     (deprecate lersif_pdivl_mulr lteif_pdivl_mulr))
+    (at level 10, only parsing).
+
+Notation lersif_pdivl_mulr :=
+  (fun b => @lersif_pdivl_mulr _ b _) (only parsing).
+
+Notation "@ 'lersif_pdivr_mulr'" :=
+  ((fun _ => @mc_1_11.lersif_pdivr_mulr)
+     (deprecate lersif_pdivr_mulr lteif_pdivr_mulr))
+    (at level 10, only parsing).
+
+Notation lersif_pdivr_mulr :=
+  (fun b => @lersif_pdivr_mulr _ b _) (only parsing).
+
+Notation "@ 'lersif_pdivl_mull'" :=
+  ((fun _ => @mc_1_11.lersif_pdivl_mull)
+     (deprecate lersif_pdivl_mull lteif_pdivl_mull))
+    (at level 10, only parsing).
+
+Notation lersif_pdivl_mull :=
+  (fun b => @lersif_pdivl_mull _ b _) (only parsing).
+
+Notation "@ 'lersif_pdivr_mull'" :=
+  ((fun _ => @mc_1_11.lersif_pdivr_mull)
+     (deprecate lersif_pdivr_mull lteif_pdivr_mull))
+    (at level 10, only parsing).
+
+Notation lersif_pdivr_mull :=
+  (fun b => @lersif_pdivr_mull _ b _) (only parsing).
+
+Notation "@ 'lersif_ndivl_mulr'" :=
+  ((fun _ => @mc_1_11.lersif_ndivl_mulr)
+     (deprecate lersif_ndivl_mulr lteif_ndivl_mulr))
+    (at level 10, only parsing).
+
+Notation lersif_ndivl_mulr :=
+  (fun b => @lersif_ndivl_mulr _ b _) (only parsing).
+
+Notation "@ 'lersif_ndivr_mulr'" :=
+  ((fun _ => @mc_1_11.lersif_ndivr_mulr)
+     (deprecate lersif_ndivr_mulr lteif_ndivr_mulr))
+    (at level 10, only parsing).
+
+Notation lersif_ndivr_mulr :=
+  (fun b => @lersif_ndivr_mulr _ b _) (only parsing).
+
+Notation "@ 'lersif_ndivl_mull'" :=
+  ((fun _ => @mc_1_11.lersif_ndivl_mull)
+     (deprecate lersif_ndivl_mull lteif_ndivl_mull))
+    (at level 10, only parsing).
+
+Notation lersif_ndivl_mull :=
+  (fun b => @lersif_ndivl_mull _ b _) (only parsing).
+
+Notation "@ 'lersif_ndivr_mull'" :=
+  ((fun _ => @mc_1_11.lersif_ndivr_mull)
+     (deprecate lersif_ndivr_mull lteif_ndivr_mull))
+    (at level 10, only parsing).
+
+Notation lersif_ndivr_mull :=
+  (fun b => @lersif_ndivr_mull _ b _) (only parsing).
+
+(* IntervalPo *)
+
+Notation "@ 'lersif_in_itv'" :=
+  ((fun _ => @mc_1_11.lersif_in_itv) (deprecate lersif_in_itv lteif_in_itv))
+    (at level 10, only parsing).
+
+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`.             *)
+Notation "@ 'itv_intersection'" :=
+  ((fun _ (R : realDomainType) => @Order.meet _ [latticeType of interval R])
+     (deprecate itv_intersection itv_meet))
+    (at level 10, only parsing) : fun_scope.
+
+Notation itv_intersection := (@itv_intersection _) (only parsing).
+
+Notation "@ 'itv_intersection1i'" :=
+  ((fun _ (R : realDomainType) => @meet1x _ [tbLatticeType of interval R])
+     (deprecate itv_intersection1i meet1x))
+    (at level 10, only parsing) : fun_scope.
+
+Notation itv_intersection1i := (@itv_intersection1i _) (only parsing).
+
+Notation "@ 'itv_intersectioni1'" :=
+  ((fun _ (R : realDomainType) => @meetx1 _ [tbLatticeType of interval R])
+     (deprecate itv_intersectioni1 meetx1))
+    (at level 10, only parsing) : fun_scope.
+
+Notation itv_intersectioni1 := (@itv_intersectioni1 _) (only parsing).
+
+Notation "@ 'itv_intersectionii'" :=
+  ((fun _ (R : realDomainType) => @meetxx _ [latticeType of interval R])
+     (deprecate itv_intersectionii meetxx))
+    (at level 10, only parsing) : fun_scope.
+
+Notation itv_intersectionii := (@itv_intersectionii _) (only parsing).
+
+(* IntervalOrdered *)
+
+Notation "@ 'itv_intersectionC'" :=
+  ((fun _ (R : realDomainType) => @meetC _ [latticeType of interval R])
+     (deprecate itv_intersectionC meetC))
+    (at level 10, only parsing) : fun_scope.
+
+Notation itv_intersectionC := (@itv_intersectionC _) (only parsing).
+
+Notation "@ 'itv_intersectionA'" :=
+  ((fun _ (R : realDomainType) => @meetA _ [latticeType of interval R])
+     (deprecate itv_intersectionA meetA))
+    (at level 10, only parsing) : fun_scope.
+
+Notation itv_intersectionA := (@itv_intersectionA _) (only parsing).
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).