diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 6ad65d62f141885cd57055735a967d34e62f6500..4498827656cfc59e8617ed895693fb7d97457fdd 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -163,7 +163,7 @@ Section auth.
     ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
   Proof. by rewrite view_auth_frac_op_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2) ↔ False.
-  Proof. rewrite view_auth_frac_op_validN. naive_solver. Qed.
+  Proof. apply view_auth_op_validN. Qed.
 
   (** The following lemmas are also stated as implications, which can be used
   to force [apply] to use the lemma in the right direction. *)
@@ -204,7 +204,7 @@ Section auth.
     by setoid_rewrite auth_view_rel_unit.
   Qed.
   Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2) ↔ False.
-  Proof. rewrite auth_auth_frac_op_valid. naive_solver. Qed.
+  Proof. apply view_auth_op_valid. Qed.
 
   (** The following lemmas are also stated as implications, which can be used
   to force [apply] to use the lemma in the right direction. *)
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 3a94b25a83963108a7b84356bda748595930f021..7cc89e9901605b667a5292486a854417d83cdea1 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -208,7 +208,7 @@ Section lemmas.
   Qed.
   Lemma gmap_view_auth_op_valid m1 m2 :
     ✓ (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
-  Proof. rewrite gmap_view_auth_frac_op_valid. naive_solver. Qed.
+  Proof. apply view_auth_op_valid. Qed.
 
   Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
   Proof.