proposition: Lemma gmultiset_elem_of_elements x X : x ∈ elements X ↔ x ∈ X.
proof: Proof. destruct X as [X]. unfold elements, gmultiset_elements. set (f xn := let '(x, n) := xn in replicate (Pos.to_nat n) x); simpl. unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl. rewrite elem_of_list_bind. split. - intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia. - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia]. exists (x,n); split; [|by apply elem_of_map_to_list]. apply elem_of_replicate; auto with lia. Qed.
imports: stdpp(gmap) stdpp(options)