proposition: Lemma meq_multeq : forall M N, M =mul= N -> forall x, x / M = x / N.
proof: Proof. unfold meq, permutation, Multiset.meq. intros M N eqMN x. rewrite !mult_comp. exact (eqMN x). Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)