diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 8a061d6894f7e2c0205cfa633ef1f55ea2c96145..81552437d27436ad2058106691a05d228e6647ae 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -194,7 +194,8 @@ Section fractional.
   Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
     frame_fractional_hyps_half.
 
-  Global Instance frame_fractional p R r Φ P q RES:
+  (* Not an instance because of performance; you can locally add it if you are willing to pay the cost. *)
+  Lemma frame_fractional p R r Φ P q RES:
     AsFractional R Φ r → AsFractional P Φ q →
     FrameFractionalHyps p R Φ RES r q →
     Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)