proposition: Lemma wf_lt_ms : well_founded lt_ms.
proof: Proof. unfold well_founded, lt_ms, lt_ms_bool. intros [p [q r]]; revert q r; pattern p; refine (well_founded_ind lt_wf _ _ p); clear p. intros p IHp q; unfold lt_mul. pattern q; apply well_founded_ind with (list nat) (trans_clos (NatMul.multiset_extension_step lt)); clear q. apply closure.wf_trans; apply NatMul.dickson; apply Wf_nat.lt_wf. intros q IHq r; pattern r; refine (well_founded_ind Wf_nat.lt_wf _ _ r); clear r. intros r IHr; apply Acc_intro. intros [p' [q' r']]; generalize (beq_nat_ok p' p); case (Nat.eqb p' p); [intro p'_eq_p | intro p'_diff_p]. subst p'; case_eq (NatMul.mult lt_bool q' q); [intro q'_eq_q | intro q'_lt_q | intro q'_gt_q | intro q'_diff_q ]. intro r'_lt_r; generalize (lt_bool_ok r' r); rewrite r'_lt_r; clear r'_lt_r; intro r'_lt_r. assert (Acc_p_q_r' := IHr _ r'_lt_r). apply Acc_intro; intros [p'' [q'' r'']]. generalize (beq_nat_ok p'' p); case (Nat.eqb p'' p); [intro p''_eq_p | intro p''_diff_p]. subst p''; case_eq (NatMul.mult lt_bool q'' q'); [intro q''_eq_q' | intro q''_lt_q' | intro q''_gt_q' | intro q''_diff_q' ]. intro r''_lt_r'; refine (Acc_inv Acc_p_q_r' _ _). rewrite (Nat.eqb_refl p). assert (q''_eq_q : NatMul.mult lt_bool q'' q = Equivalent). apply NatMul.mult_is_complete_equiv. transitivity q'. assert (H := NatMul.mult_is_sound _ _ lt_bool_ok q'' q'); rewrite q''_eq_q' in H; exact H. assert (H := NatMul.mult_is_sound _ _ lt_bool_ok q' q); rewrite q'_eq_q in H; exact H. rewrite q''_eq_q; assumption. intros _; assert (q''_lt_q : NatMul.mult lt_bool q'' q = Less_than). assert (H := NatMul.mult_is_sound _ _ lt_bool_ok q' q); rewrite q'_eq_q in H. assert (H' := NatMul.mult_is_sound _ _ lt_bool_ok q'' q'); rewrite q''_lt_q' in H'. assert (H'' : trans_clos (NatMul.multiset_extension_step lt) q'' q). apply NatMul.list_permut_trans_clos_multiset_extension_step_2 with q'; trivial. assert (H3 := NatMul.mult_is_sound _ _ lt_bool_ok q'' q). apply NatMul.mult_is_complete_less_than with lt. exact lt_bool_ok. exact Nat.lt_trans. exact Nat.lt_irrefl. assumption. apply IHq. assert (H := NatMul.mult_is_sound lt _ lt_bool_ok q'' q); rewrite q''_lt_q in H; exact H. intros; discriminate. intros; discriminate. intro p''_lt_p; apply IHp; generalize (lt_bool_ok p'' p); rewrite p''_lt_p; trivial. intros _; apply IHq. assert (H := NatMul.mult_is_sound _ _ lt_bool_ok q' q); rewrite q'_lt_q in H; exact H. intros; discriminate. intros; discriminate. intro p'_lt_p; apply IHp; generalize (lt_bool_ok p' p); rewrite p'_lt_p; 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)