proposition: Theorem zerop_red_spoly_l : forall a b : poly A0 eqA ltM, zerop a -> forall Q : list (poly A0 eqA ltM), red (spolyp a b) Q.
proof: Proof. intros a b; (case a; case b). intros x c0 x0 c1; generalize c0 c1; case x; case x0; simpl in |- *; auto. intros c2 c3 H' Q; unfold red in |- *; simpl in |- *; auto. intros a0 l c2 c3 H'; elim H'. intros a0 l c2 c3 H' Q; unfold red in |- *; simpl in |- *; auto. intros a0 l a1 l0 c2 c3 H'; elim H'. Qed.
imports: Buchberger(moreCoefStructure)