proposition: Theorem rstar_rtopO : forall (Q : list (poly A0 eqA ltM)) (p : list (Term A n)), canonical A0 eqA ltM p -> reduceplus A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q p (pO A n) -> reducestar A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q p (pO A n).
proof: Proof. Proof using plusA os cs. intros Q p H' H'0. elim reduce0_reducestar with (1 := cs) (eqA_dec := eqA_dec) (ltM_dec := ltM_dec) (Q := Q) (p := pO A n); auto. intros t E; apply reducestar0; auto. apply pO_irreducible; auto. Qed.
imports: Buchberger(moreCoefStructure)