proposition: Theorem eqT_zerop_is_eqTerm : forall a b : Term, eqT a b -> zeroP a -> zeroP b -> eqTerm a 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 := A0); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)