diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 467b9f90cd1c695b3d2ab0e5c16ef6f9e404d63e..7df5ef405a90123ef77dca3a226b8f9d53417092 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -177,6 +177,12 @@ Section gen_heap.
   Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
   Proof. rewrite mapsto_eq. apply ghost_map_elem_persist. Qed.
 
+  (** Framing support *)
+  Global Instance frame_mapsto p l v q1 q2 RES :
+    FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
+    Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
+  Proof. apply: frame_fractional. Qed.
+
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).
   Proof. rewrite meta_token_eq. apply _. Qed.
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 81552437d27436ad2058106691a05d228e6647ae..9b48116c8ac43250d1f60c7b2889a1b782dca1bb 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -194,11 +194,13 @@ Section fractional.
   Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
     frame_fractional_hyps_half.
 
-  (* Not an instance because of performance; you can locally add it if you are willing to pay the cost. *)
+  (* Not an instance because of performance; you can locally add it if you are
+  willing to pay the cost. We have concrete instances for certain fractional
+  assertions such as ↦. *)
   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. *)
+    Frame p R P RES.
   Proof.
     rewrite /Frame=>-[HR _][->?]H.
     revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 1c4d73212719176c83e45444075d63fb1581a3b3..0e80ada63a78541a97c6b73c5e050b5486fd5cc2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -373,6 +373,14 @@ Section mapsto_tests.
     l ↦{#1 / 2} v -∗  ∃ q, l ↦{#1 / 2 + q} v.
   Proof. iIntros "H". iExists _. iSplitL; first by iAssumption. Abort.
 
+  Lemma mapsto_frame_1 l v q1 q2 :
+    l ↦{#q1} v -∗ l ↦{#q2} v -∗ l ↦{#q1 + q2} v.
+  Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.
+
+  Lemma mapsto_frame_2 l v q :
+    l ↦{#q/2} v -∗ l ↦{#q/2} v -∗ l ↦{#q} v.
+  Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.
+
 End mapsto_tests.
 
 Section inv_mapsto_tests.