proposition: Lemma meq_union_meq M N P : M + P =mul= N + P -> M =mul= N.
proof: Proof. intros; try_solve_meq. assert (((x/M)%msets + (x/P)%msets)%nat = ((x/N)%msets + (x/P)%msets)%nat). rewrite <- !union_mult. apply meq_multeq; trivial. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)