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