diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index b6d415b1480f96330ee568d9ccdef6595679d088..a2235f1a6f2a2cb1c82c225bc138c226331d521b 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -132,6 +132,10 @@ Section heap.
     rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
   Qed.
 
+  Lemma heap_mapsto_op_split l q v :
+    (l ↦{q} v)%I ≡ (l ↦{q/2} v ★ l ↦{q/2} v)%I.
+  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
+
   (** Weakest precondition *)
   Lemma wp_alloc N E e v P Φ :
     to_val e = Some v →