diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 6343b8ee6f32e37157ab7d315525987fa62f4d7a..d0c4f0fac1f246a3bd3c2d73df9e07d49eaf99c2 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -79,12 +79,6 @@ Section heap.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
   Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
 
-  Lemma heap_mapsto_valid l q v : l ↦{q} v ⊢ ✓ q.
-  Proof.
-    rewrite heap_mapsto_eq /heap_mapsto_def auth_own_valid !discrete_valid.
-    by apply pure_mono=> /singleton_valid [??].
-  Qed.
-
   Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
   Proof.
     by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
@@ -125,6 +119,15 @@ Section heap.
   Lemma heap_ex_mapsto_op_half l q : l ↦{q/2} - ∗ l ↦{q/2} - ⊣⊢ l ↦{q} -.
   Proof. by rewrite heap_ex_mapsto_op Qp_div_2. Qed.
 
+  Lemma heap_mapsto_valid l q v : l ↦{q} v ⊢ ✓ q.
+  Proof.
+    rewrite heap_mapsto_eq /heap_mapsto_def auth_own_valid !discrete_valid.
+    by apply pure_mono=> /singleton_valid [??].
+  Qed.
+  Lemma heap_mapsto_valid_2 l q1 q2 v1 v2 :
+    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ✓ (q1 + q2)%Qp.
+  Proof. rewrite heap_mapsto_op heap_mapsto_valid. auto with I. Qed.
+
   (** Weakest precondition *)
   Lemma wp_alloc E e v :
     to_val e = Some v → nclose heapN ⊆ E →