diff --git a/CHANGELOG.md b/CHANGELOG.md
index 57a15c2fb11983e2e1ef060cbd282808c61f4499..efce126461ce7c8ea5bd71174841f79b265e0503 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,9 @@ lemma.
   The old `to_frac_agree` and its lemmas still exist, except that the
   `frac_agree_op_valid` lemmas are made bi-directional.
 * Rename typeclass instance `Later_inj` -> `Next_inj`.
+* Remove `view_auth_frac_op`, `auth_auth_frac_op`, `gmap_view_auth_frac_op`; the
+  corresponding `dfrac` lemmas can be used instead (together with `dfrac_op_own`
+  if needed).
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 5a0aca78953ba0a2f4bd119d64c137f9e3ed6efe..00f829c2f3c4f1a935c3e0269c743036efbf57a3 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -120,8 +120,6 @@ Section auth.
   (** Operation *)
   Lemma auth_auth_dfrac_op dq1 dq2 a : ●{dq1 ⋅ dq2} a ≡ ●{dq1} a ⋅ ●{dq2} a.
   Proof. apply view_auth_dfrac_op. Qed.
-  Lemma auth_auth_frac_op q1 q2 a : ●{#(q1 + q2)} a ≡ ●{#q1} a ⋅ ●{#q2} a.
-  Proof. apply view_auth_frac_op. Qed.
   Global Instance auth_auth_dfrac_is_op dq dq1 dq2 a :
     IsOp dq dq1 dq2 → IsOp' (●{dq} a) (●{dq1} a) (●{dq2} a).
   Proof. rewrite /auth_auth. apply _. Qed.
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 6ebf62a342bd1c487c28d59bfe00a93720151c83..3109af96ad37acfcb813975e150a7fbca940bc2d 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -180,10 +180,6 @@ Section lemmas.
     gmap_view_auth (dp ⋅ dq) m ≡
     gmap_view_auth dp m â‹… gmap_view_auth dq m.
   Proof. by rewrite /gmap_view_auth view_auth_dfrac_op. Qed.
-  Lemma gmap_view_auth_frac_op p q m :
-    gmap_view_auth (DfracOwn (p + q)) m ≡
-    gmap_view_auth (DfracOwn p) m â‹… gmap_view_auth (DfracOwn q) m.
-  Proof. by rewrite /gmap_view_auth view_auth_frac_op. Qed.
   Global Instance gmap_view_auth_dfrac_is_op dq dq1 dq2 m :
     IsOp dq dq1 dq2 → IsOp' (gmap_view_auth dq m) (gmap_view_auth dq1 m) (gmap_view_auth dq2 m).
   Proof. rewrite /gmap_view_auth. apply _. Qed.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 0d7106419f861bdef9c70221f2a5c44ee09e4ae1..ce5b96b9c9aadf1a302bc517fc42a15a124af0d2 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -275,8 +275,6 @@ Section cmra.
     intros; split; simpl; last by rewrite left_id.
     by rewrite -Some_op -pair_op agree_idemp.
   Qed.
-  Lemma view_auth_frac_op q1 q2 a : ●V{#(q1 + q2)} a ≡ ●V{#q1} a ⋅ ●V{#q2} a.
-  Proof. rewrite -dfrac_op_own. apply view_auth_dfrac_op. Qed.
   Global Instance view_auth_dfrac_is_op dq dq1 dq2 a :
     IsOp dq dq1 dq2 → IsOp' (●V{dq} a) (●V{dq1} a) (●V{dq2} a).
   Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_dfrac_op. Qed.
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index e59bb24129b138f54c798d1f8a69709b5f3b8587..ac9a1dc0f5901242d0e43054ab530630463a9834 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -157,7 +157,7 @@ Section lemmas.
   Global Instance ghost_map_auth_timeless γ q m : Timeless (ghost_map_auth γ q m).
   Proof. unseal. apply _. Qed.
   Global Instance ghost_map_auth_fractional γ m : Fractional (λ q, ghost_map_auth γ q m)%I.
-  Proof. intros p q. unseal. rewrite -own_op gmap_view_auth_frac_op //. Qed.
+  Proof. intros p q. unseal. rewrite -own_op -gmap_view_auth_dfrac_op //. Qed.
   Global Instance ghost_map_auth_as_fractional γ q m :
     AsFractional (ghost_map_auth γ q m) (λ q, ghost_map_auth γ q m)%I q.
   Proof. split; first done. apply _. Qed.