proposition: Lemma gmultiset_choose_or_empty X : (∃ x, x ∈ X) ∨ X = ∅.
proof: Proof. destruct (elements X) as [|x l] eqn:HX; [right|left]. - by apply gmultiset_elements_empty_iff. - exists x. rewrite <-gmultiset_elem_of_elements, HX. by left. Qed.
imports: stdpp(gmap) stdpp(options)