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