fact: Fixpoint lt_bool (n1 n2 : nat) {struct n1} := match n1, n2 with | O, O => false | O, (S _) => true | (S m1), (S m2) => lt_bool m1 m2 | (S _), O => false 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)