proposition: Lemma mord_sorder : strict_order MultisetGt.
proof: Proof. exact (Build_strict_order mord_trans mord_irreflex). Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)