diff --git a/algebra/frac.v b/algebra/frac.v
index 6bd8528ebc899307ab7ec8f5f8a0902cbb3c5f4f..11cb32deab537850a9a6977cd4e385dab7f04ccd 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -35,6 +35,3 @@ 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 9d0b2e481abae93db713df70621cd5baf723f093..f54b034357e9e87642ff26744038ee179e6f61c9 100644
--- a/prelude/numbers.v
+++ b/prelude/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.