From 680b21c4a47930e71df326701c079104780c9143 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 1 Oct 2020 10:17:40 +0200
Subject: [PATCH] add version of Qp_lower_bound that returns less-than facts

---
 theories/numbers.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/numbers.v b/theories/numbers.v
index 644f0490..451da9f8 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -790,6 +790,12 @@ Proof.
   apply Qp_eq; simpl. unfold Qcdiv. ring.
 Qed.
 
+Lemma Qp_lower_bound_lt (q1 q2 : Qp) : ∃ q : Qp, q < q1 ∧ q < q2.
+Proof.
+  destruct (Qp_lower_bound q1 q2) as (qmin & q1' & q2' & [-> ->]).
+  exists qmin. split; eapply Qp_lt_sum; eauto.
+Qed.
+
 Lemma Qp_cross_split p a b c d :
   (a + b = p → c + d = p →
   ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
-- 
GitLab