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