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