proposition: Theorem div_is_T1 : forall (a : Term A n) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a), eqTerm (A:=A) eqA (n:=n) (divTerm a nZa) (T1 A1 n).
proof: Proof. Proof using plusA multA minusA invA cs. intros a; case a; simpl in |- *; auto. intros a0 m nZa; split; auto. apply divA_A1 with (1 := cs). unfold M1 in |- *; apply mult_div_id; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)