proposition: Lemma mult_remove_not_in : forall M a x, ~ x =A= a -> x / (rem a M) = x / M.
proof: Proof. induction M; intros. auto. simpl; destruct (eqA_dec a0 a). destruct (eqA_dec x a); solve [absurd (x =A= a); eauto with sets | trivial]. simpl; destruct (eqA_dec x a). rewrite (IHM a0 x); trivial. apply IHM; trivial. Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)