proposition: Lemma member_dec a M : {a in M}+{~a in M}.
proof: Proof. intros; case (Compare_dec.zerop (mult a M)); intro. right; mset_unfold; lia. left; auto. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)