proposition: Theorem Grobner_imp_SpolyQ : forall Q : list (poly A0 eqA ltM), Grobner Q -> SpolyQ A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q.
proof: Proof. Proof using os cs. intros Q H'; elim H'. intros H'1. apply SpolyQ0; auto. intros p q H'0 H'2 H'3 H'4. elim reduce0_reducestar with (ltM_dec := ltM_dec) (eqA_dec := eqA_dec) (1 := cs) (Q := Q) (p := spolyf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec p q H'2 H'4); auto. intros t E; apply Spoly_10 with (Cp := H'2) (Cq := H'4); auto. apply reducestar_eqp_com with (1 := cs) (p := spolyf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec p q H'2 H'4) (q := t); auto. apply spolyf_canonical with (1 := cs); auto. apply H'1 with (p := spolyf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec p q H'2 H'4); auto. apply CombLinear_spoly; auto. apply spolyf_canonical with (1 := cs); auto. Qed.