proposition: Lemma diff_perm_single : forall x a b M N, x / (M - (a::b::N)) = x / (M - (b::a::N)).
proof: Proof. intros x a b M N. simpl; apply diff_mult_comp. apply multeq_meq. intro x'; apply remove_perm_single. Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)