fact: Definition lt_mul : (relation (list nat)) := trans_clos (NatMul.multiset_extension_step lt).
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)