proposition: Lemma lex_le_lt : forall p1 p2 p3 q1 q2 q3, p1 <= q1 -> dickson.NatMul.mult lt_bool p2 q2 = Less_than -> lt_ms (p1,(p2,p3)) (q1,(q2,q3)).
proof: Proof. intros p1 p2 p3 q1 q2 q3 p1_le_q1 p2_lt_q2; 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]. rewrite p2_lt_q2; trivial. generalize (lt_bool_ok p1 q1); case (lt_bool p1 q1). reflexivity. intro Abs; apply False_rect; apply p1_diff_q1. clear p1_diff_q1; revert p1 q1 p1_le_q1 Abs ; fix lex_le_lt 1. intro p1; case p1; clear p1. intros q1 _; case q1; clear q1. intros _; reflexivity. intros n Abs; apply False_rect; apply Abs; apply le_n_S; apply Nat.le_0_l. intros p1 q1; case q1; clear q1. intro Abs; inversion Abs. intros q1 Hle Hnot_lt; apply f_equal. apply lex_le_lt. apply le_S_n; assumption. intro H; apply Hnot_lt; apply le_n_S; 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)