Add the eqType instance for intervals, le_bound(l|r)_anti, and itv_intersection, redefine prev_of_itv and itv_decompose using lersif, extend itv_rewrite, simplify proofs (#271)

2 files changed, 182 insertions, 133 deletions

diff --git a/ChangeLog b/ChangeLog
index 49a850a..81d479a 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -14,7 +14,10 @@
 
 	* Extended theory about homo and mono for leq/or and Num.le
 
-	* Extended theory of lersif and intervals
+	* Changed and extended theory of lersif and intervals:
+	  * Many lersif related lemmas are ported from ssrnum
+	  * Definitions that changed: prev_of_itv, itv_decompose, and itv_rewrite
+	  * Theory of intersections of intervals is added
 
 	* Renamed: (together with the _in suffix counterpart)
 	  mono_inj -> incr_inj
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 498c415..3ef444c 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -232,54 +232,36 @@ 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 => H /=; rewrite lter_pdivl_mulr. Qed.
+Proof. by case: b => ? /=; rewrite lter_pdivl_mulr. Qed.
 
 Lemma lersif_pdivr_mulr : 0 < z -> y / z <= x ?< if b = (y <= x * z ?< if b).
-Proof. by case: b => H /=; rewrite lter_pdivr_mulr. Qed.
+Proof. by case: b => ? /=; rewrite lter_pdivr_mulr. Qed.
 
 Lemma lersif_pdivl_mull : 0 < z -> x <= z^-1 * y ?< if b = (z * x <= y ?< if b).
-Proof. by case: b => H /=; rewrite lter_pdivl_mull. Qed.
+Proof. by case: b => ? /=; rewrite lter_pdivl_mull. Qed.
 
 Lemma lersif_pdivr_mull : 0 < z -> z^-1 * y <= x ?< if b = (y <= z * x ?< if b).
-Proof. by case: b => H /=; rewrite lter_pdivr_mull. Qed.
+Proof. by case: b => ? /=; rewrite lter_pdivr_mull. Qed.
 
 Lemma lersif_ndivl_mulr : z < 0 -> x <= y / z ?< if b = (y <= x * z ?< if b).
-Proof. by case: b => H /=; rewrite lter_ndivl_mulr. Qed.
+Proof. by case: b => ? /=; rewrite lter_ndivl_mulr. Qed.
 
 Lemma lersif_ndivr_mulr : z < 0 -> y / z <= x ?< if b = (x * z <= y ?< if b).
-Proof. by case: b => H /=; rewrite lter_ndivr_mulr. Qed.
+Proof. by case: b => ? /=; rewrite lter_ndivr_mulr. Qed.
 
 Lemma lersif_ndivl_mull : z < 0 -> x <= z^-1 * y ?< if b = (y <=z * x ?< if b).
-Proof. by case: b => H /=; rewrite lter_ndivl_mull. Qed.
+Proof. by case: b => ? /=; rewrite lter_ndivl_mull. Qed.
 
 Lemma lersif_ndivr_mull : z < 0 -> z^-1 * y <= x ?< if b = (z * x <= y ?< if b).
-Proof. by case: b => H /=; rewrite lter_ndivr_mull. Qed.
+Proof. by case: b => ? /=; rewrite lter_ndivr_mull. Qed.
 
 End LersifField.
 
-Section IntervalPo.
-
 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.
 
-Variable R : numDomainType.
-
-Definition pred_of_itv (i : interval R) : pred R :=
-  [pred x | let: Interval l u := i in
-      match l with
-        | BOpen a => a < x
-        | BClose a => a <= x
-        | BInfty => true
-      end &&
-      match u with
-        | BOpen b => x < b
-        | BClose b => x <= b
-        | BInfty => true
-      end].
-Canonical Structure itvPredType := Eval hnf in mkPredType pred_of_itv.
-
 (* 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.
@@ -300,30 +282,84 @@ Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _))
 Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _))
   (at level 0, format "`] -oo ,  '+oo' [") : ring_scope.
 
+Section IntervalEq.
+
+Variable T : eqType.
+
+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 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.
+
+Canonical itv_bound_eqMixin := EqMixin eq_itv_boundP.
+Canonical itv_bound_eqType :=
+  Eval hnf in 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 := Eval hnf in EqType (interval T) interval_eqMixin.
+
+End IntervalEq.
+
+Section IntervalPo.
+
+Variable R : numDomainType.
+
+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 := Eval hnf in mkPredType pred_of_itv.
+
 (* 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)
+       | 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)
+       | 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)
+         (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)
+         (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)
+         (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.
@@ -331,32 +367,30 @@ Definition itv_rewrite (i : interval R) x : Type :=
 Definition itv_decompose (i : interval R) x : Prop :=
   let: Interval l u := i in
   ((match l with
-    | BClose a => (a <= x) : Prop
-    | BOpen a => (a < x) : Prop
+    | BOpen_if b lb => (lb <= x ?< if b) : Prop
     | BInfty => True
   end : Prop) *
   (match u with
-    | BClose b => (x <= b) : Prop
-    | BOpen b => (x < b) : Prop
+    | 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=> x [[[] a|] [[] b|]]; apply: (iffP andP); case. Qed.
+Proof. by move=> ? [[? ?|] [? ?|]]; apply: (iffP andP); case. Qed.
 
 Arguments itv_dec {x i}.
 
 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 b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if ~~ b2 && b1
     | BOpen_if _ _, BInfty => false
     | _, _ => true
   end.
 
 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)
+    | BOpen_if b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if ~~ b1 && b2
     | BInfty, BOpen_if _ _ => false
     | _, _ => true
   end.
@@ -364,7 +398,7 @@ Definition le_boundr (b1 b2 : itv_bound R) :=
 Lemma itv_boundlr bl br x :
   (x \in Interval bl br) =
   (le_boundl bl (BClose x)) && (le_boundr (BClose x) br).
-Proof. by move: bl br => [[] a|] [[] b|]. Qed.
+Proof. by case: bl br => [? ? |] []. Qed.
 
 Lemma le_boundl_refl : reflexive le_boundl.
 Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed.
@@ -378,16 +412,14 @@ Hint Resolve le_boundr_refl : core.
 
 Lemma le_boundl_trans : transitive le_boundl.
 Proof.
-move=> [lb1 lr1 |] [lb2 lr2 |] [lb3 lr3 |] //= H H0.
-apply: {H H0} (lersif_imply _ (lersif_trans H H0)).
-by case: lb1; case: lb2; case: lb3.
+by move=> [[] x|] [[] y|] [[] z|] lexy leyz //;
+  apply: (lersif_imply _ (lersif_trans lexy leyz)).
 Qed.
 
 Lemma le_boundr_trans : transitive le_boundr.
 Proof.
-move=> [lb1 lr1 |] [lb2 lr2 |] [lb3 lr3 |] //= H H0.
-apply: {H H0} (lersif_imply _ (lersif_trans H H0)).
-by case: lb1; case: lb2; case: lb3.
+by move=> [[] x|] [[] y|] [[] z|] lexy leyz //;
+  apply: (lersif_imply _ (lersif_trans lexy leyz)).
 Qed.
 
 Lemma le_boundl_bb x b1 b2 :
@@ -398,49 +430,66 @@ 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.
 
+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.
+
+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.
+
 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 1?eq_sym (eqr_le, lter_anti).
-Qed.
+Proof. by move: bl br => [] [] y /=; rewrite !inE lersif_anti. Qed.
 
 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=> hx y; rewrite itv_boundlr inE /=.
-by apply/negP => /andP [] /lersif_trans hy /hy {hy}; rewrite lersifNF.
+move=> ? y; rewrite itv_boundlr inE /=.
+by apply/negP => /andP [] lexay /(lersif_trans lexay); rewrite lersifNF.
 Qed.
 
 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 [[] xb|] //=; rewrite inE lterr. Qed.
+Proof. by move=> [] xa [b xb|]; rewrite inE lersifxx. Qed.
 
 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 [[] xa|] //=; rewrite inE lterr ?andbT ?andbF. Qed.
+Proof. by move=> [] xb [b xa|]; rewrite inE lersifxx /= ?andbT ?andbF. Qed.
 
 Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
 
 Lemma itvP : forall (x : R) (i : interval R), x \in i -> itv_rewrite i x.
 Proof.
-move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //;
-  do ?[by rewrite ltrW | by rewrite ltrWN | by rewrite ltrNW |
-    by rewrite (ltr_geF, ler_gtF)]];
-  rewrite ?(bound_in_itv) /le_boundl /le_boundr //=; do ?
-    [ by rewrite (@ler_trans _ x)
-    | by rewrite 1?ltrW // (@ltr_le_trans _ x)
-    | by rewrite 1?ltrW // (@ler_lt_trans _ x) // 1?ltrW
-    | by apply: negbTE; rewrite ler_gtF // (@ler_trans _ x)
-    | by apply: negbTE; rewrite ltr_geF // (@ltr_le_trans _ x) // 1?ltrW
-    | by apply: negbTE; rewrite ltr_geF // (@ler_lt_trans _ x)].
+move=> x [[[] a|] [[] b|]] /itv_dec // [? ?];
+  do ?split => //; rewrite ?bound_in_itv /le_boundl /le_boundr //=;
+  do 1?[apply/negbTE; rewrite (ler_gtF, ltr_geF) //];
+  by [ rewrite ltrW
+     | rewrite (@ler_trans _ x) // 1?ltrW
+     | rewrite (@ltr_le_trans _ x)
+     | rewrite (@ler_lt_trans _ x) // 1?ltrW ].
 Qed.
 
 Hint Rewrite intP : core.
 Arguments itvP [x i].
 
+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').
+
+Definition itv_intersection1i : left_id `]-oo, +oo[ itv_intersection.
+Proof. by case=> i []. Qed.
+
+Definition itv_intersectioni1 : right_id `]-oo, +oo[ itv_intersection.
+Proof. by case=> [[lb lr |] [ub ur |]]. Qed.
+
+Lemma itv_intersectionii : idempotent itv_intersection.
+Proof. by case=> [[[] lr |] [[] ur |]] //=; rewrite !lerr. Qed.
+
 Definition subitv (i1 i2 : interval R) :=
   match i1, i2 with
     | Interval a1 b1, Interval a2 b2 => le_boundl a2 a1 && le_boundr b1 b2
@@ -448,57 +497,48 @@ Definition subitv (i1 i2 : interval R) :=
 
 Lemma subitvP : forall (i2 i1 : interval R), subitv i1 i2 -> {subset i1 <= i2}.
 Proof.
-by move=> [[[] a2|] [[] b2|]] [[[] a1|] [[] b1|]];
-  rewrite /subitv //; case/andP=> /= ha hb x hx; rewrite ?inE;
-    rewrite ?(ler_trans ha) ?(ler_lt_trans ha) ?(ltr_le_trans ha) //;
-      rewrite ?(ler_trans _ hb) ?(ltr_le_trans _ hb) ?(ler_lt_trans _ hb) //;
-        rewrite ?(itvP hx) //.
+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.
 
-Lemma subitvPr : forall (a b1 b2 : itv_bound R),
+Lemma subitvPr (a b1 b2 : itv_bound R) :
   le_boundr b1 b2 -> {subset (Interval a b1) <= (Interval a b2)}.
-Proof. by move=> a b1 b2 hb; apply: subitvP=> /=; rewrite hb andbT. Qed.
+Proof. by move=> leb; apply: subitvP; rewrite /= leb andbT. Qed.
 
-Lemma subitvPl : forall (a1 a2 b : itv_bound R),
+Lemma subitvPl (a1 a2 b : itv_bound R) :
   le_boundl a2 a1 -> {subset (Interval a1 b) <= (Interval a2 b)}.
-Proof. by move=> a1 a2 b ha; apply: subitvP=> /=; rewrite ha /=. Qed.
+Proof. by move=> lea; apply: subitvP; rewrite /= lea /=. Qed.
 
-Lemma lersif_in_itv : forall ba bb xa xb x,
+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 move=> ba bb xa xb y; rewrite itv_boundlr; case/andP; apply: lersif_trans.
-Qed.
+Proof. by case: ba bb => [] [] /itvP /= ->. Qed.
 
-Lemma ltr_in_itv : forall ba bb xa xb x, ba || bb ->
-  x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> xa < xb.
-Proof.
-move=> ba bb xa xb x; case bab: (_ || _) => // _.
-by move/lersif_in_itv; rewrite bab.
-Qed.
+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.
 
-Lemma ler_in_itv : forall ba bb xa xb x,
+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=> ba bb xa xb x; move/lersif_in_itv; move/lersifW. Qed.
+Proof. by move/lersif_in_itv/lersifW. Qed.
 
-Lemma mem0_itvcc_xNx : forall x, (0 \in `[-x, x]) = (0 <= x).
-Proof.
-by move=> x; rewrite !inE; case hx: (0 <= _); rewrite (andbT, andbF) ?ge0_cp.
-Qed.
+Lemma mem0_itvcc_xNx x : (0 \in `[-x, x]) = (0 <= x).
+Proof. by rewrite !inE /= oppr_le0 andbb. Qed.
 
-Lemma mem0_itvoo_xNx : forall x, 0 \in `](-x), x[ = (0 < x).
-Proof.
-by move=> x; rewrite !inE; case hx: (0 < _); rewrite (andbT, andbF) ?gt0_cp.
-Qed.
+Lemma mem0_itvoo_xNx x : 0 \in `](-x), x[ = (0 < x).
+Proof. by rewrite !inE /= oppr_lt0 andbb. Qed.
 
-Lemma itv_splitI : forall a b, forall x,
-  x \in Interval a b = (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b).
-Proof. by move=> [[] a|] [[] b|] x; rewrite ?inE ?andbT. Qed.
+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.
 
 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 move: ba bb => [] []; rewrite ?inE lter_oppr andbC lter_oppl. Qed.
+Proof. by rewrite !inE lersif_oppr andbC lersif_oppl. Qed.
 
 Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[).
 Proof. exact: oppr_itv. Qed.
@@ -514,27 +554,6 @@ Proof. exact: oppr_itv. Qed.
 
 End IntervalPo.
 
-Notation BOpen := (BOpen_if true).
-Notation BClose := (BOpen_if false).
-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.
-
 Section IntervalOrdered.
 
 Variable R : realDomainType.
@@ -550,19 +569,18 @@ Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b ->
     (y \in Interval a (BOpen_if (~~ bc) xc))
     || (y \in Interval (BOpen_if bc xc) b).
 Proof.
-move=> hxc y; rewrite !itv_boundlr [le_boundr]lock /=.
-have [la /=|nla /=] := boolP (le_boundl a _); rewrite -lock.
-  have [lb /=|nlb /=] := boolP (le_boundr _ b); rewrite ?andbT ?andbF ?orbF //.
-    by case: bc => //=; case: ltrgtP.
-  symmetry; apply: contraNF nlb; rewrite /le_boundr /=.
-  case: b hxc => // bb xb hxc hyc.
-  suff /(lersif_trans hyc) : xc <= xb ?< if bb.
-    by case: bc {hyc} => //= /lersifS.
-  by case: a bb hxc {la} => [[] ?|] [] /= /itvP->.
-symmetry; apply: contraNF nla => /andP [hc _].
-case: a hxc hc => [[] xa|] hxc; rewrite /le_boundl //=.
-  by move=> /lersifW /(ltr_le_trans _) -> //; move: b hxc=> [[] ?|] /itvP->.
-by move=> /lersifW /(ler_trans _) -> //; move: b hxc=> [[] ?|] /itvP->.
+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.
 
 Lemma itv_splitU2 (x : R) a b : x \in Interval a b ->
@@ -575,6 +593,34 @@ rewrite (@itv_splitU x true _ _ _ y); first by rewrite itv_xx inE.
 by move: xab; rewrite boundl_in_itv itv_boundlr => /andP [].
 Qed.
 
+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.
+
+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.
+
+Canonical itv_intersection_monoid :=
+  Monoid.Law itv_intersectionA (@itv_intersection1i R) (@itv_intersectioni1 R).
+
+Canonical itv_intersection_comoid := Monoid.ComLaw itv_intersectionC.
+
 End IntervalOrdered.
 
 Section IntervalField.
@@ -584,13 +630,13 @@ Variable R : realFieldType.
 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 /= hx; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltrW.
+by move=> [] [] xa xb /= ?; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltrW.
 Qed.
 
 Lemma mid_in_itvoo : forall (xa xb : R), xa < xb -> mid xa xb \in `]xa, xb[.
-Proof. by move=> xa xb hx; apply: mid_in_itv. Qed.
+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 hx; apply: mid_in_itv. Qed.
+Proof. by move=> xa xb ?; apply: mid_in_itv. Qed.
 
 End IntervalField.