diff --git a/CHANGELOG.md b/CHANGELOG.md
index 49070971fb2f02fae5c3f50f18a43fb3dc556c2c..65d1afd3a9e7897f12692260a5fc374b8096a32e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -73,6 +73,9 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
 * Rename typeclass instances of CMRA operational typeclasses (`Op`, `Core`,
   `PCore`, `Valid`, `ValidN`, `Unit`) to have a `_instance` suffix, so that
   their original names are available to use as lemma names.
+* Rename `frac_valid'`→`frac_valid`, `frac_op'`→`frac_op`,
+  `ufrac_op'`→`ufrac_op`. Those names were previously blocked by typeclass
+  instances.
 
 **Changes in `bi`:**
 
@@ -253,6 +256,8 @@ s/\bcmraT\b/cmra/g
 s/\bCmraT\b/Cmra/g
 s/\bucmraT\b/ucmra/g
 s/\bUcmraT\b/Ucmra/g
+# u?frac_op/valid lemmas
+s/\b(u?frac_(op|valid))'/\1/g
 EOF
 ```
 
diff --git a/iris/algebra/frac.v b/iris/algebra/frac.v
index 433b86a4ef76a36620b05972b9bdc923b8838b7a..06115f125d98c8b437d39a100ef564f5b5affef3 100644
--- a/iris/algebra/frac.v
+++ b/iris/algebra/frac.v
@@ -19,9 +19,9 @@ Section frac.
   Local Instance frac_pcore_instance : PCore frac := λ _, None.
   Local Instance frac_op_instance : Op frac := λ x y, (x + y)%Qp.
 
-  Lemma frac_valid' p : ✓ p ↔ (p ≤ 1)%Qp.
+  Lemma frac_valid p : ✓ p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
-  Lemma frac_op' p q : p â‹… q = (p + q)%Qp.
+  Lemma frac_op p q : p â‹… q = (p + q)%Qp.
   Proof. done. Qed.
   Lemma frac_included p q : p ≼ q ↔ (p < q)%Qp.
   Proof. by rewrite Qp_lt_sum. Qed.
@@ -32,7 +32,7 @@ Section frac.
   Definition frac_ra_mixin : RAMixin frac.
   Proof.
     split; try apply _; try done.
-    intros p q. rewrite !frac_valid' frac_op'=> ?.
+    intros p q. rewrite !frac_valid frac_op=> ?.
     trans (p + q)%Qp; last done. apply Qp_le_add_l.
   Qed.
   Canonical Structure fracR := discreteR frac frac_ra_mixin.
@@ -51,5 +51,5 @@ Section frac.
   Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
   Proof. done. Qed.
   Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
-  Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.
+  Proof. by rewrite /IsOp' /IsOp frac_op Qp_div_2. Qed.
 End frac.
diff --git a/iris/algebra/ufrac.v b/iris/algebra/ufrac.v
index 144646382b3ba4864baf47b675733030a348c140..66adffbcbb991d68538d07a29f3031f2e8b9cac5 100644
--- a/iris/algebra/ufrac.v
+++ b/iris/algebra/ufrac.v
@@ -18,7 +18,7 @@ Section ufrac.
   Local Instance ufrac_pcore_instance : PCore ufrac := λ _, None.
   Local Instance ufrac_op_instance : Op ufrac := λ x y, (x + y)%Qp.
 
-  Lemma ufrac_op' p q : p â‹… q = (p + q)%Qp.
+  Lemma ufrac_op p q : p â‹… q = (p + q)%Qp.
   Proof. done. Qed.
   Lemma ufrac_included p q : p ≼ q ↔ (p < q)%Qp.
   Proof. by rewrite Qp_lt_sum. Qed.
@@ -39,5 +39,5 @@ Section ufrac.
   Proof. intros p _. apply Qp_add_id_free. Qed.
 
   Global Instance is_op_ufrac q : IsOp' q (q/2)%Qp (q/2)%Qp.
-  Proof. by rewrite /IsOp' /IsOp ufrac_op' Qp_div_2. Qed.
+  Proof. by rewrite /IsOp' /IsOp ufrac_op Qp_div_2. Qed.
 End ufrac.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 9989cafd4bf67e9651a866021084c42ce8a0464f..47ecc5bdca7e99b624349c817e4ad924a37e77fa 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -518,7 +518,7 @@ Section cmra.
   Proof.
     rewrite !local_update_unital.
     move=> Hup Hrel n [[[q ag]|] bf] /view_both_validN Hrel' [/=].
-    - rewrite right_id -Some_op -pair_op frac_op'=> /Some_dist_inj [/= H1q _].
+    - rewrite right_id -Some_op -pair_op frac_op=> /Some_dist_inj [/= H1q _].
       by destruct (Qp_add_id_free 1 q).
     - rewrite !left_id=> _ Hb0.
       destruct (Hup n bf) as [? Hb0']; [by eauto using view_rel_validN..|].
diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 322dc616c1818ad315f3618e191f06a9961b8dd1..8d943d4ff146bd8b114b2508fe2d5444e4c76a72 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -23,7 +23,7 @@ Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
 Proof. by uPred.unseal. Qed.
 
 Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
-Proof. rewrite uPred.discrete_valid frac_valid' //. Qed.
+Proof. rewrite uPred.discrete_valid frac_valid //. Qed.
 
 Section gmap_ofe.
   Context `{Countable K} {A : ofe}.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 65a617639548268aa212b511e8106e8fb2ef029c..72d1e4dccaf6a824c37da4403fe6d9c668e08d85 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -45,7 +45,7 @@ Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) =>
 Lemma pending_split γ q :
   own γ (Pending q) ⊣⊢ own γ (Pending (q/2)) ∗ own γ (Pending (q/2)).
 Proof.
-  rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op' Qp_div_2 //.
+  rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op Qp_div_2 //.
 Qed.
 
 Lemma pending_shoot γ n :