proposition: Theorem unit_nZ : forall p : poly A0 eqA ltM, ~ zeroP (A:=A) A0 eqA (n:=n) (unit p).
proof: Proof. Proof using plusA multA minusA invA cs. intros p; case p. intros x; case x; simpl in |- *; auto. intros a l; case a; simpl in |- *; auto. Qed.
imports: Buchberger(moreCoefStructure)