From 62389c827d72c63981d568cb2875559f43fb95da Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Tue, 4 Oct 2016 17:50:57 +0200
Subject: [PATCH] tweak the Qp lemmas

---
 theories/numbers.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/numbers.v b/theories/numbers.v
index 23e4697b..9ce89535 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -567,9 +567,12 @@ Proof.
   apply Qp_eq; simpl. ring.
 Qed.
 
-Lemma Qp_ge_1 (q: Qp): ¬ ((1 + q)%Qp ≤ 1%Qp)%Qc.
+Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp ≤ 1%Qp)%Qc.
 Proof.
   intros Hle.
   apply (Qcplus_le_mono_l q 0 1) in Hle.
-  apply Qcle_ngt in Hle. by destruct q.
+  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
 Qed.
+
+Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc.
+Proof. apply Qclt_le_weak, Qp_prf. Qed.
-- 
GitLab