diff --git a/theories/numbers.v b/theories/numbers.v
index 644f04904f884b81573154f08c06e9cf5dd92741..451da9f8183cbd38eb7d5228831f8934175af002 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.