proposition: Lemma union_isempty M N : M + N =mul= empty -> M =mul= empty.
proof: Proof. intros; try_solve_meq. assert (((x/M)%msets + (x/N)%msets)%nat = x/empty). rewrite <- (meq_multeq H); auto with multisets. rewrite empty_mult in H0. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)