Remove unused Qp argument to dfrac_valid_discarded

CHANGELOG.md

@@ -73,6 +73,7 @@ lemma.
   and `saved_pred_own`, so they can be updated. The previous persistent versions
   can be recovered with the fraction `DfracDiscarded`. Allocation lemmas now take
   a `dq` parameter to define the initial fraction.
+* Remove an unused fraction argument to `dfrac_valid_discarded`.
 
 **Changes in `program_logic`:**
 

iris/algebra/dfrac.v

@@ -173,7 +173,7 @@ Section dfrac.
   Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
   Proof. rewrite comm. apply dfrac_valid_own_r. Qed.
 
-  Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
+  Lemma dfrac_valid_discarded : ✓ DfracDiscarded.
   Proof. done. Qed.
 
   Lemma dfrac_valid_own_discarded q :