proposition: Theorem divP_eqT : forall a b c : Term A n, eqT a b -> ~ zeroP (A:=A) A0 eqA (n:=n) b -> divP a c -> divP b c.
proof: Proof. Proof using plusA minusA invA cs A1. intros a b c H' nZb H'1; inversion H'1. apply divTerm_def with (nZb := nZb0); auto. apply divTerm_eqT with (a := a); auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)