proposition: Lemma mord_irreflex: forall M, ~ M >mul M.
proof: Proof. unfold not; intros M MgtM. assert (M + empty >mul M + empty); [ rewrite (union_empty M); trivial | idtac]. absurd (empty >mul empty). apply empty_min. rewrite_rl (mord_ext_l empty empty M); trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)