proposition: Theorem divTerm_rew : forall (a b : Term A n) (nZ1 nZ2 : ~ zeroP (A:=A) A0 eqA (n:=n) b), divTerm a nZ1 = divTerm a nZ2.
proof: Proof. Proof using plusA multA minusA invA cs A1. intros a b; case a; case b; simpl in |- *; auto. intros a0 m a1 m0 nZ1 nZ2. rewrite divA_rew with (1 := cs) (nZ2 := nZ2); auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)