proposition: Theorem eqTerm_divTerm_comp : 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), eqTerm (A:=A) eqA (n:=n) a b -> eqTerm (A:=A) eqA (n:=n) c d -> eqTerm (A:=A) eqA (n:=n) (divTerm a nZc) (divTerm b nZd).
proof: Proof. Proof using plusA multA minusA invA cs A1. intros a b c d; case a; case b; case c; case d; simpl in |- *; auto. intros A0' c0 d2 c2 d3 c3 d4 c4 nZd2 H'0 H'1 H'2. case H'2; intros H'3 H'4; clear H'2. case H'1; intros H'2 H'5; clear H'1. split; auto. rewrite H'5; rewrite H'4; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)