proposition: Theorem canonical_pX_eqT : forall a b p, canonical (pX a p) -> eqT a b -> ~ zeroP (A:=A) A0 eqA (n:=n) b -> canonical (pX b p).
proof: Proof. intros a b p H' H'0 H'1. split; auto. apply olist_pX_eqT with (a := a); auto. simpl in |- *; split; auto. case H'; simpl in |- *; intuition. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)