proposition: Lemma wf_lt_exc_pb_ok : well_founded lt_exc_pb_ok.
proof: Proof. apply (wf_inverse_image (exc_pb_ok) _ lt_weight_exc_pb_ok weight_exc_pb_ok). unfold well_founded, lt_weight_exc_pb_ok. intros [n m]; generalize m; clear m; pattern n. refine (well_founded_ind lt_wf _ _ n). clear n; intros n IHn m; apply Acc_intro. intros [n' m']; generalize (beq_nat_ok n' n); case (Nat.eqb n' n); [intro n'_eq_n; subst n' | intro n'_diff_n]. revert m'; pattern m; refine (well_founded_ind wf_lt_ms _ _ m); clear m. intros m IHm m' m'_lt_m; apply Acc_intro. intros [n'' m'']; generalize (beq_nat_ok n'' n); case (Nat.eqb n'' n); [intro n''_eq_n | intro n''_diff_n]. subst n''; apply IHm; trivial. intro n''_lt_n; apply IHn; trivial. intro n'_lt_n; apply IHn; trivial. 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)