proposition: Lemma multiplicity_difference X Y x : multiplicity x (X ∖ Y) = multiplicity x X - multiplicity x Y.
proof: Proof. destruct X as [X], Y as [Y]; unfold multiplicity; simpl. rewrite lookup_difference_with. destruct (X !! _), (Y !! _); simplify_option_eq; lia. Qed.
imports: stdpp(gmap) stdpp(options)