proposition: Theorem divTerm_on_eqT_eqT : forall a b : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) a -> forall nZb : ~ zeroP (A:=A) A0 eqA (n:=n) b, eqT a b -> eqT (divTerm a nZb) (T1 A1 n).
proof: Proof. intros a b; case a; case b; unfold eqT in |- *; simpl in |- *; auto. intros b2 c b3 c0 H' H'0 H'1; rewrite H'1; auto. rewrite mult_div_id; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)