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