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