proposition: Lemma mord_trans: forall X Y Z, X >mul Y -> Y >mul Z -> X >mul Z.
proof: Proof. intros X Y Z oXY oYZ. compute; constructor 2 with Y; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)