proposition: Lemma gmultiset_size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y.
proof: Proof. intros HX%gmultiset_disj_union_difference. rewrite HX at 2; rewrite gmultiset_size_disj_union. lia. Qed.
imports: stdpp(gmap) stdpp(options)