proposition: Lemma transitive_le_mpo : transitive le_mpo.
proof: Proof. intros s t u MPOst MPOtu; elim MPOst; clear MPOst; intro MPOst. subst t; hyp. elim MPOtu; clear MPOtu; intro MPOtu. subst t; right; hyp. right; apply transitive_lt_mpo with t; hyp. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)