proposition: Lemma lt_bool_ok : forall n1 n2, if lt_bool n1 n2 then n1 < n2 else ~n1 < n2.
proof: Proof. fix lt_bool_ok 1. intro n1; case n1; clear n1. intros [ | n2]; simpl. apply Nat.lt_irrefl. apply le_n_S; apply Nat.le_0_l. intros n1 [ | n2]; simpl. apply Nat.nle_succ_0. generalize (lt_bool_ok n1 n2); case (lt_bool n1 n2). intro H; apply le_n_S; assumption. intros H1 H2; apply H1; apply le_S_n; assumption. Defined.
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)