diff --git a/CHANGELOG.md b/CHANGELOG.md
index e5362c59b4fd8cd2eb6446b5f2c3876e113ac5d3..8152693b159cb34cceaf3c4383f9e218c4e81fb1 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 9c1c0ab5382db57b7310cee1a03dad69f9c7611a..3976a72bfe94d659e48956945bf9d166cf48760d 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.