proposition: Lemma diff_perm : forall M N a x, x / ((rem a M) - N) = x / (rem a (M - N)).
proof: Proof. intros M N; gen M; clear M. induction N. auto. intros M b x. change (rem b M - (a::N)) with (M - (b::a::N)). rewrite diff_perm_single. simpl; apply IHN. Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)