And also a variant when having to mapstos.

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 →