proposition: Theorem inP_reducestar : forall P Q : list (poly A0 eqA ltM), (forall a : list (Term A n), inPolySet A A0 eqA n ltM a Q -> inPolySet A A0 eqA n ltM a P) -> forall a b : list (Term A n), reducestar A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q a b -> reduceplus A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec P a b.
proof: Proof. intros P Q H' a b H'0; inversion H'0; auto. apply inP_reduceplus with (Q := Q); auto. Qed.
imports: Buchberger(moreCoefStructure)