proposition: Lemma mOrd_wf : well_founded ltA -> well_founded MultisetLT.
proof: Proof. intro wf_lt; constructor; intros; apply mOrd_acc. intros; exact (wf_lt x). Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)