proposition: Lemma gmultiset_elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y.
proof: Proof. intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union. by apply submseteq_inserts_r. Qed.
imports: stdpp(gmap) stdpp(options)