diff --git a/algebra/auth.v b/algebra/auth.v
index 8abc1dede9ce5bef3a622ede122e13767c679bcd..5a103b2313559d0ca2d81a8acfdda368e813a045 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -132,9 +132,11 @@ Canonical Structure authR : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
 Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
 Proof.
   split; first apply _.
-  intros [[] ?]; rewrite /= /cmra_valid /cmra_validN /=
-    -?cmra_discrete_included_iff -?cmra_discrete_valid_iff; auto.
-Admitted.
+  intros [[] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
+  - setoid_rewrite <-cmra_discrete_included_iff.
+    rewrite -cmra_discrete_valid_iff. tauto.
+  - by rewrite -cmra_discrete_valid_iff.
+Qed.
 
 (** Internalized properties *)
 Lemma auth_equivI {M} (x y : auth A) :