proposition: Theorem zeroP_comp_eqTerm : forall a b : Term, zeroP a -> eqTerm a b -> zeroP b.
proof: Proof. Proof using plusA multA minusA invA divA cs A1. intros a b; case a; case b; simpl in |- *; auto. intuition. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := a1); auto; apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)