proposition: Theorem divP_inv2 : forall a b : Term A n, divP a b -> ~ zeroP (A:=A) A0 eqA (n:=n) b.
proof: Proof. intros a b H; inversion H; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)