proposition: Lemma empty_min_red: forall M, ~(empty >mul_1 M).
proof: Proof. intros M empty_red_M; inversion empty_red_M. apply not_empty with (X + {{a}}) a; auto with multisets. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)