proposition: Lemma gmultiset_eq X Y : X = Y ↔ ∀ x, multiplicity x X = multiplicity x Y.
proof: Proof. split; [by intros ->|intros HXY]. destruct X as [X], Y as [Y]; f_equal; apply map_eq; intros x. specialize (HXY x); unfold multiplicity in *; simpl in *. repeat case_match; naive_solver lia. Qed.
imports: stdpp(gmap) stdpp(options)