proposition: Lemma empty_min: forall M, ~(empty >mul M).
proof: Proof. intros M empty_lt_M; case (RelUtil.tc_step_l empty_lt_M). intro M_red_empty; apply empty_min_red with M; trivial. intro step; destruct step; apply empty_min_red with x; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)