From 2e98600dd7d0e0f155fcf01714ff2d8b421ac4af Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Tue, 4 Oct 2016 15:27:57 +0200
Subject: [PATCH] Add lemmas about Qp and fraction

---
 algebra/frac.v    | 3 +++
 prelude/numbers.v | 7 +++++++
 2 files changed, 10 insertions(+)

diff --git a/algebra/frac.v b/algebra/frac.v
index 11cb32dea..6bd8528eb 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -35,3 +35,6 @@ Global Instance frac_full_exclusive : Exclusive 1%Qp.
 Proof.
   move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
 Qed.
+
+Lemma invalid_plus_q: ∀ (q: Qp), ¬ ✓ (1 + q)%Qp.
+Proof. intros q H. by apply (Qp_ge_1 q). Qed.
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 05c66b458..9d0b2e481 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -566,3 +566,10 @@ Proof.
   exists (mk_Qp (q2 - q1 / 2%Z) Hq2'). split; [by rewrite Qp_div_2|].
   apply Qp_eq; simpl. ring.
 Qed.
+
+Lemma Qp_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.
+Qed.
-- 
GitLab