proposition: Lemma lt_as_red: same_relation MultisetLt clos_transM_RedLt.
proof: Proof. exact (RelUtil.tc_transp MultisetRedGt). Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)