From efed1800a4f2eaa942704ab8bebc60d9a3ac8dfd Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Sat, 30 May 2020 05:29:37 +0200
Subject: General theory of min and max, and use in ssrnum

- min and max can now be used in a partial order (sometimes under preconditions)
- min and max can now be used in a numDomainType (sometimes under preconditions)
---
 mathcomp/algebra/interval.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'mathcomp/algebra/interval.v')

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 3ed2825..950546b 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -210,19 +210,19 @@ Proof. by case: b; apply lter_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 /= ltexI. Qed.
+Proof. by case: b; rewrite /= (le_minr, lt_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 /= lteIx. Qed.
+Proof. by case: b; rewrite /= (le_minl, lt_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 /= ltexU. Qed.
+Proof. by case: b; rewrite /= (le_maxr, lt_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 /= lteUx. Qed.
+Proof. by case: b; rewrite /= (le_maxl, lt_maxl). Qed.
 
 End LersifOrdered.
 
-- 
cgit v1.2.3