proposition: Theorem zerop_red : forall (a : poly A0 eqA ltM) (aP : list (poly A0 eqA ltM)), zerop (nf a aP) -> red a aP.
proof: Proof. intros a aP H'. apply nf_red with (aP := aP); auto with datatypes. generalize H'; case (nf a aP); simpl in |- *; auto. intros x; case x; simpl in |- *; auto. intros c H'0; red in |- *; simpl in |- *; auto. intros a0 l H'0 H'1; elim H'1; auto. Qed.
imports: Buchberger(moreCoefStructure)