proposition: Theorem reducetopO_pO : forall Q : list (poly A0 eqA ltM), reducestar A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (pO A n) (pO A n).
proof: Proof. intros Q; apply reducestar0; auto. apply Rstar_0; auto. Qed.
imports: Buchberger(moreCoefStructure)