proposition: Theorem eqT_divTerm : forall (a b c d : Term A n) (nZc : ~ zeroP (A:=A) A0 eqA (n:=n) c) (nZd : ~ zeroP (A:=A) A0 eqA (n:=n) d), eqT a b -> eqT c d -> eqT (divTerm a nZc) (divTerm b nZd).
proof: Proof. intros a b c d; case a; case b; case c; case d; unfold eqT in |- *; simpl in |- *; auto. intros A0' c0 d2 c2 H' c3 H'0 c4 H'1 H'2 H'3 H'4; rewrite H'3; rewrite H'4; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)