proposition: Theorem divTerm_nZ : forall a b : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) a -> forall nZb : ~ zeroP (A:=A) A0 eqA (n:=n) b, ~ zeroP (A:=A) A0 eqA (n:=n) (divTerm a nZb).
proof: Proof. Proof using plusA multA minusA invA cs A1. intros a b; case a; case b; simpl in |- *; auto. intros a0 m a1 m0 H nZb; apply divA_nZ with (1 := cs); auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)