proposition: Lemma mred_irreflex: forall M, ~M >mul_1 M.
proof: Proof. unfold not; intros. absurd (M >mul M); [apply mord_irreflex | constructor; trivial]. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)