diff --git a/CHANGELOG.md b/CHANGELOG.md
index c655bd855c70f1872aecd978c4c5742129cf06c1..fb45428e8a709162f5f36d1be4b31eb5d3bf42ac 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -38,6 +38,7 @@ Coq 8.13 is no longer supported.
     use the tactic `dist_later_intro`/`dist_later_fin_intro` to introduce it.
   (by Michael Sammler, Lennard Gäher, and Simon Spies).
 * Add `max_Z` and `mono_Z` cameras.
+* Add `dfrac_valid`.
 
 **Changes in `bi`:**
 
@@ -135,7 +136,10 @@ Coq 8.13 is no longer supported.
 * Refactor soundness lemmas: `bupd_plain_soundness` → `bupd_soundness`,
   `soundness` → `laterN_soundness` + `pure_soundness`; removed
   `consistency_modal`.
-* Strengthen `cmra_valid_elim` to `✓ a ⊢ ⌜ ✓{0} a ⌝`; make `discrete_valid` a derived law.
+* Strengthen `cmra_valid_elim` to `✓ a ⊢ ⌜ ✓{0} a ⌝`; make `discrete_valid` a
+  derived law.
+* Remove `frac_validI`. Instead, move to the pure context (with `%` in the proof
+  mode or `uPred.discrete_valid` in manual proofs) and use `frac_valid`.
 
 **Changes in `heap_lang`:**
 
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index f44745158f10a3ec6e61f4380b423e38d22150ce..d582389ba908faa0e84dd92fcc1427364b5c7e7c 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -104,6 +104,14 @@ Section dfrac.
     | DfracBoth q, DfracBoth q' => DfracBoth (q + q')
     end.
 
+  Lemma dfrac_valid dq :
+    ✓ dq ↔ match dq with
+           | DfracOwn q => q ≤ 1
+           | DfracDiscarded => True
+           | DfracBoth q => q < 1
+           end%Qp.
+  Proof. done. Qed.
+
   Lemma dfrac_op_own q p : DfracOwn p â‹… DfracOwn q = DfracOwn (p + q).
   Proof. done. Qed.
 
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.