proposition: Theorem red_id : forall (a : poly A0 eqA ltM) (aL : list (poly A0 eqA ltM)), red (spolyp a a) aL.
proof: Proof. intros a P; case a. unfold red in |- *; simpl in |- *; auto. intros x H'. apply rstar_rtopO; auto. apply spolyf_canonical with (1 := cs); auto. apply Rstar_0; auto. apply spolyf_pO with (1 := cs); auto. Qed.
imports: Buchberger(moreCoefStructure)