proposition: Theorem zeroP_divTerm : 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 d H' A0' H'0 H'1 nZd; auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := divA A0 d nZd); auto. apply divA_A0_l with (1 := cs). Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)