proposition: Lemma multiplicity_intersection X Y x : multiplicity x (X ∩ Y) = multiplicity x X `min` multiplicity x Y.
proof: Proof. destruct X as [X], Y as [Y]; unfold multiplicity; simpl. rewrite lookup_intersection_with. destruct (X !! _), (Y !! _); simpl; lia. Qed.
imports: stdpp(gmap) stdpp(options)