diff --git a/CHANGELOG.md b/CHANGELOG.md
index 61ee78e400705d3975e15fd1a276e7fb0527151f..93c63457d4938ee0cf79099e96d621bc207f2810 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -130,6 +130,8 @@ With this release, we dropped support for Coq 8.9.
   `⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝`.
 * Change `gen_heap_init` to also return ownership of the points-to facts for the
   initial heap.
+* Rename `mapsto_mapsto_ne` to `mapsto_frac_ne`, and add a simpler
+  `mapsto_ne` that does not require reasoning about fractions.
 
 **Changes in `program_logic`:**
 
@@ -159,6 +161,8 @@ s/\bauth_both_frac_valid\b/auth_both_frac_valid_discrete/g
 # gen_heap_ctx and proph_map_ctx
 s/\bgen_heap_ctx\b/gen_heap_interp/g
 s/\bproph_map_ctx\b/proph_map_interp/g
+# other gen_heap changes
+s/\bmapsto_mapsto_ne\b/mapsto_frac_ne/g
 EOF
 ```
 
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index d368da7b6ee96e781f21f455b142099606e7ea5e..73d9aa5a5b3570cc223e1d1ea92778bc9b2e8b67 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -172,12 +172,14 @@ Section gen_heap.
     iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
   Qed.
 
-  Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
+  Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
     ¬ (q1 + q2 ≤ 1)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof.
     iIntros (?) "Hl1 Hl2"; iIntros (->).
     by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
   Qed.
+  Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+  Proof. apply mapsto_frac_ne, Qp_not_add_le_l. Qed.
 
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 425121877339991ce7a8ae1cb6960eefd42d3ef9..ce297d8e6eeca46222ac65b49b069b2d8b2f9b2a 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -294,9 +294,11 @@ Proof.
   iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
 Qed.
 
-Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
+Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
   ¬ (q1 + q2 ≤ 1)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
-Proof. apply mapsto_mapsto_ne. Qed.
+Proof. apply mapsto_frac_ne. Qed.
+Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+Proof. apply mapsto_ne. Qed.
 
 Global Instance inv_mapsto_own_proper l v :
   Proper (pointwise_relation _ iff ==> (≡)) (inv_mapsto_own l v).