proposition: Lemma empty_dec : forall M, {M =mul= empty}+{M <>mul empty}.
proof: Proof. apply mset_ind_type with (P := fun M => {M =mul= empty}+{M <>mul empty}). left; solve_meq. intros M a cmp; right; intro emp. absurd (a/(M + {{a}}) = a/empty); auto with multisets. rewrite empty_mult; rewrite union_mult. set (w := singleton_member a); unfold member in w. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)