diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 7d4cd6154294132d3b71d7f16c7bd8f8d2382eef..b6fc071c4063b7bb5ed05bdb7f6269697d9b7bea 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -105,17 +105,4 @@ Section frac_auth.
   Proof.
     intros. by apply auth_update, option_local_update, prod_local_update_2.
   Qed.
-
-  Lemma frac_auth_update_alloc q a b c :
-    (∀ n : nat, ✓{n} a → ✓{n} (c ⋅ a)) →
-    ●! a ⋅ ◯!{q} b ~~> ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b).
-  Proof. intros ?. by apply frac_auth_update, op_local_update. Qed.
-
-  Lemma frac_auth_dealloc q a b c `{!Cancelable c} :
-    ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b) ~~> ●! a ⋅ ◯!{q} b.
-  Proof.
-    apply frac_auth_update.
-    move=> n [x|] /= Hvalid Heq; split; eauto using cmra_validN_op_r.
-    eapply (cancelableN c); by rewrite ?assoc.
-  Qed.
 End frac_auth.