proposition: Lemma union_mult : forall M N x, (x/(M + N))%msets = ((x/M)%msets + (x/N)%msets)%nat.
proof: Proof. induction M; auto. intros N x; simpl. destruct (eqA_dec x a); auto. rewrite IHM. auto. Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)