fact: Definition lt_weight_exc_pb_ok (w1 w2 : nat * (nat * (list nat * nat))) := match w1, w2 with | (n1,m1), (n2,m2) => if Nat.eqb n1 n2 then lt_ms m1 m2 else n1 < n2 end.
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)