From 028eb93c107b3f103c577e28a4e4b2c2544229f6 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Fri, 2 Oct 2020 13:00:54 +0200
Subject: [PATCH] Remove Qp_not_plus_q_ge_1

---
 CHANGELOG.md       | 9 +++++++++
 theories/numbers.v | 3 ---
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e5362c59..8152693b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,15 @@ API-breaking change is listed.
   and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.
 - Add `max` and `min` operations for `Qp`.
 - Add additional lemmas for `Qp`.
+- Remove the lemma `Qp_not_plus_q_ge_1` in favor of `Qp_not_plus_ge`.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
+```
+sed -i '
+s/\bQp_not_plus_q_ge_1\b/Qp_not_plus_ge/g
+' $(find theories -name "*.v")
+```
 
 ## std++ 1.4.0 (released 2020-07-15)
 
diff --git a/theories/numbers.v b/theories/numbers.v
index 9c1c0ab5..3976a72b 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -838,9 +838,6 @@ Proof.
   apply Hle, Qp_prf.
 Qed.
 
-Lemma Qp_not_plus_q_ge_1 (q: Qp) : ¬ (1 + q)%Qp ≤ 1%Qp.
-Proof. apply Qp_not_plus_ge. Qed.
-
 Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc.
 Proof. apply Qclt_le_weak, Qp_prf. Qed.
 
-- 
GitLab