proposition: Theorem divTerm_on_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 -> eqTerm (A:=A) eqA (n:=n) a (multTerm (A:=A) multA (n:=n) (divTerm a nZb) b).
proof: Proof. Proof using plusA minusA invA cs A1. intros a b; case a; case b; unfold eqT in |- *; simpl in |- *; auto. intros d c A0' c0 H' H'0 H'1; rewrite <- H'1. split; auto. apply divA_is_multA with (1 := cs); auto. rewrite mult_div_id; auto. rewrite mult_mon_zero_l; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)