proposition: Lemma gmultiset_elements_empty_iff X : elements X = [] ↔ X = ∅.
proof: Proof. split; [|intros ->; by rewrite gmultiset_elements_empty]. destruct X as [X]; unfold elements, gmultiset_elements; simpl. intros; apply (f_equal GMultiSet). destruct (map_to_list X) as [|[x p]] eqn:?; simpl in *. - by apply map_to_list_empty_iff. - pose proof (Pos2Nat.is_pos p). destruct (Pos.to_nat); naive_solver lia. Qed.
imports: stdpp(gmap) stdpp(options)