proposition: Lemma gmultiset_size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
proof: Proof. intros Hsz. destruct (gmultiset_choose_or_empty X) as [|HX]; [done|]. contradict Hsz. rewrite HX, gmultiset_size_empty; lia. Qed.
imports: stdpp(gmap) stdpp(options)