Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼`

See discussion in !305 (comment 71807)

I decided to use Iris's names and argument because:

• It's shorter
• Iris's singleton_included lemmas have been there for longer than the multiset lemmas, so are (probably) more widely used

theories/gmultiset.v

@@ -568,8 +568,17 @@ Section more_lemmas.
   Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y.
   Proof. multiset_solver. Qed.
 
-  Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[+ x +]} ⊆ X.
+  Lemma gmultiset_singleton_subseteq_l x X : {[+ x +]} ⊆ X ↔ x ∈ X.
   Proof. multiset_solver. Qed.
+  Lemma gmultiset_singleton_subseteq x y :
+    {[+ x +]} ⊆@{gmultiset A} {[+ y +]} ↔ x = y.
+  Proof.
+    split; [|multiset_solver].
+    (* FIXME: [multiset_solver] should solve this *)
+    intros Hxy. specialize (Hxy x).
+    rewrite multiplicity_singleton, multiplicity_singleton' in Hxy.
+    case_decide; [done|lia].
+  Qed.
 
   Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
   Proof. multiset_solver. Qed.