diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index b44fb1ef80e7b75f80c0f5d6b91ec3d36aab5aca..5e2e7b45820351d0e67f902fa5514ddf35e1e79f 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -30,7 +30,7 @@ Section upred.
     ✓ dq ⊣⊢ match dq with
             | DfracOwn q => ⌜q ≤ 1⌝%Qp
             | DfracBoth q => ⌜q < 1⌝%Qp
-            | _ => True
+            | DfracDiscarded => True
             end.
   Proof. destruct dq; by rewrite uPred.discrete_valid. Qed.