diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6fa4af042bca7f9cb2406eec14ca878c3f53d85c..714f5c5d1e7e4b22dad118ea65deafdf565da27c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,6 +8,8 @@ API-breaking change is listed.
 - Strengthen `map_disjoint_difference_l` and `map_disjoint_difference_l`, and
   thereby make them consistent with the corresponding lemmas for sets.
 - Add support for compiling the packages with dune. (by Rodolphe Lepigre)
+- Add lemmas `gset_to_gmap_singleton`, `difference_union_intersection`,
+  `difference_union_intersection_L`. (by Léo Stefanesco)
 
 ## std++ 1.10.0 (2024-04-12)
 
diff --git a/stdpp/gmap.v b/stdpp/gmap.v
index 1e58b2487b12efdeda832c75d88e83e05e68c705..8f28f260ae2072322102b963034912ad0e5734fc 100644
--- a/stdpp/gmap.v
+++ b/stdpp/gmap.v
@@ -739,6 +739,12 @@ Section gset.
     rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
       elem_of_singleton; destruct (decide (i = j)); intuition.
   Qed.
+  Lemma gset_to_gmap_singleton {A} (x : A) i :
+    gset_to_gmap x {[ i ]} = {[i:=x]}.
+  Proof.
+    rewrite <-(right_id_L ∅ (∪) {[ i ]}), gset_to_gmap_union_singleton.
+    by rewrite gset_to_gmap_empty.
+  Qed.
   Lemma gset_to_gmap_difference_singleton {A} (x : A) i Y :
     gset_to_gmap x (Y ∖ {[i]}) = delete i (gset_to_gmap x Y).
   Proof.
diff --git a/stdpp/sets.v b/stdpp/sets.v
index a675cb22278e19c04e58544e9a35f313c94de52f..7957836fbdbc127c9f4c1e684396d4e6e7b72c6f 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -820,6 +820,8 @@ Section set.
     Qed.
     Lemma difference_difference_r X Y Z : X ∖ (Y ∖ Z) ≡ (X ∖ Y) ∪ (X ∩ Z).
     Proof. intros x. destruct (decide (x ∈ Z)); set_solver. Qed.
+    Lemma difference_union_intersection X Y : (X ∖ Y) ∪ (X ∩ Y) ≡ X.
+    Proof. rewrite union_intersection_l, difference_union. set_solver. Qed.
 
     Lemma subseteq_disjoint_union X Y : X ⊆ Y ↔ ∃ Z, Y ≡ X ∪ Z ∧ X ## Z.
     Proof.
@@ -855,6 +857,8 @@ Section set.
     Proof. unfold_leibniz. apply singleton_union_difference. Qed.
     Lemma difference_difference_r_L X Y Z : X ∖ (Y ∖ Z) = (X ∖ Y) ∪ (X ∩ Z).
     Proof. unfold_leibniz. apply difference_difference_r. Qed.
+    Lemma difference_union_intersection_L X Y : (X ∖ Y) ∪ (X ∩ Y) = X.
+    Proof. unfold_leibniz. apply difference_union_intersection. Qed.
 
   End dec_leibniz.
 End set.