proposition: Lemma empty_decomp_dec : forall M, {Ma: (Multiset * A) | M =mul= fst Ma + {{snd Ma}}} + {M =mul= empty}.
proof: Proof. induction M using mset_ind_type. right; auto with multisets. left; exists (M, a); auto with multisets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)