fact: Variables (A : Type) (Multiset : Type) (meq : relation Multiset) (mult : A -> Multiset -> nat) (diff : Multiset -> Multiset -> Multiset) (diff_mult : forall M N x, mult x (diff M N) = mult x M - mult x N).
imports: Coq(Relations Psatz)