From 5e809e16078d4659cd2dbb6c1bbc754fa6d3b6ee Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Thu, 14 Jan 2021 13:50:52 +0900
Subject: itv_bound comparison with -oo/+oo

---
 mathcomp/algebra/interval.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 067a457..4a1cadb 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -217,6 +217,14 @@ 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.
 
+Lemma ge_pinftyE b : (+oo <= b) = (b == +oo). Proof. by move: b => [|[]]. Qed.
+
+Lemma le_ninftyE b : (b <= -oo) = (b == -oo). Proof. by case: b => // - []. Qed.
+
+Lemma gt_pinfty b : (+oo < b) = false. Proof. by []. Qed.
+
+Lemma lt_ninfty b : (b < -oo) = false. Proof. by case: b => // -[]. Qed.
+
 Definition subitv i1 i2 :=
   let: Interval b1l b1r := i1 in
   let: Interval b2l b2r := i2 in (b2l <= b1l) && (b1r <= b2r).
-- 
cgit v1.2.3