diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 34fba7aef020814d4962c814d86c4a8402456d6b..e3272890bcf3d76d53b368bef2f46b04a96cfc10 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -23,9 +23,6 @@ Section upred.
     ✓ g ⊣⊢ ∀ i, ✓ g i.
   Proof. by uPred.unseal. Qed.
 
-  Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
-  Proof. rewrite uPred.discrete_valid frac_valid //. Qed.
-
   Section gmap_ofe.
     Context `{Countable K} {A : ofe}.
     Implicit Types m : gmap K A.
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 913ddb925efa5ad49a2e154207746d41fe073e82..e9df6b26d52aad304753036e35b16db6fd55f04a 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -47,7 +47,7 @@ Section proofs.
   Proof. split; [done|]. apply _. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
-  Proof. rewrite -frac_validI. apply (own_valid_2 γ q1 q2). Qed.
+  Proof. rewrite -frac_valid -uPred.discrete_valid. apply (own_valid_2 γ q1 q2). Qed.
 
   Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
   Proof.