proposition: Theorem ltP_pX_olist : forall a p, olist p -> ltP p (pX a pO) -> olist (pX a p).
proof: Proof. intros a p; case p; auto. intros H' H'1; unfold olist, DescA, consA in |- *; simpl in |- *; unfold consA, nilA in |- *. apply d_one; auto. intros b l H' H'0. apply olist_cons; auto. 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); auto. injection H2; intros H'1 H'2; rewrite H'1; auto. unfold pO in |- *; intros H'3 H'4; inversion H'4. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)