proposition: Theorem ltP_trans : forall x y z, ltP x y -> ltP y z -> ltP x z.
proof: Proof. Proof using os. intros x y z H'; generalize z; clear z; elim H'. intros x0 p z; case z; auto. intros H'0; inversion H'0. intros x0 y0 p q H'0 z H'1; simple inversion H'1. discriminate H. rewrite <- H1. intros H'2; try assumption. apply ltP_hd; auto. apply ltT_trans with (y := y0); auto. injection H0. intros H'3 H'4; rewrite <- H'4; auto. rewrite <- H2. intros H'2 H'3; apply ltP_hd; auto. apply ltT_eqTl with (a := x1); auto. injection H1. intros H'4 H'5; rewrite H'5; auto. intros x0 y0 p q H'0 H'1 H'2 z H'3; simple inversion H'3. discriminate H. rewrite <- H1; auto. intros H'4; apply ltP_hd; auto. apply ltT_eqTr with (a := y0). apply (eqT_sym A n); auto. injection H0. intros H'5 H'6; rewrite <- H'6; auto. rewrite <- H2. intros H'4 H'5; apply ltP_tl; auto. apply (eqT_trans A n) with (y := x1); auto. injection H1. intros H'6 H'7; rewrite H'7; auto. apply H'2; auto. injection H1. intros H'6; rewrite <- H'6; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)