proposition: Theorem ltp_not_refl : forall x, ~ ltP x x.
proof: Proof. Proof using os. intros x; elim x. red in |- *; intros H'; inversion H'. intros a l H'; red in |- *; intros H'0; simple inversion H'0. discriminate H. injection H1. injection H0. intros H'1 H'2 H'3 H'4; rewrite H'2; rewrite H'4; intros H'5. apply (ltT_not_refl a); auto. injection H1; injection H2. intros H'1 H'2 H'3 H'4; rewrite H'1; rewrite H'3; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)