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