proposition: Lemma lex_lt : forall p1 p2 p3 q1 q2 q3, p1 < q1 -> lt_ms (p1,(p2,p3)) (q1,(q2,q3)).
proof: Proof. intros p1 p2 p3 q1 q2 q3 p1_lt_q1; unfold lt_ms, lt_ms_bool. generalize (beq_nat_ok p1 q1); case (Nat.eqb p1 q1); [intro p1_eq_q1 | intro p1_diff_q1]; trivial. absurd (S p1 <= p1); subst; trivial; auto with arith. generalize (lt_bool_ok p1 q1); case (lt_bool p1 q1). reflexivity. intro Abs; apply False_rect; apply Abs; 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)