proposition: Theorem reds_SpolyQ : forall (P : list (poly A0 eqA ltM)) (a b : poly A0 eqA ltM), reds a b P -> Spoly_1 A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec P (s2p A A0 eqA n ltM a) (s2p A A0 eqA n ltM b).
proof: Proof. intros P a b H'; elim H'; auto. intros P0 a0 b0 H'0; cut (red A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec (spolyp A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os b0 a0) P0); auto. case a0; case b0; unfold red in |- *; simpl in |- *; auto. intros x H'1 x0 H'2 H'3; inversion H'3. apply Spoly_10 with (Cp := H'2) (Cq := H'1); auto. apply red_com; auto. intros P0 a0 b0 c. case c; case b0; case a0; simpl in |- *. intros x; case x; simpl in |- *; auto. intros c0 x0 c1 x1 c2 H'0 H'1 H'2 H'3 H'4 H'5; elim H'5. intros a1 l c0 x0; case x0; simpl in |- *. intros c1 x1 c2 H'0 H'1 H'2 H'3 H'4 H'5; elim H'5. intros a2 l0 c1 x1; case x1; simpl in |- *. intros c2 H'0 H'1 H'2 H'3 H'4 H'5; elim H'5. intros a3 l1 c2 H'0 H'1 H'2 H'3 H'4 H'5. change (Spoly_1 A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec P0 (pX a1 l) (pX a2 l0)) in |- *. apply Spoly_11 with (d := a3) (t := l1); auto. change (inPolySet A A0 eqA n ltM (s2p A A0 eqA n ltM (mks A A0 eqA n ltM (pX a3 l1) c2)) P0) in |- *. apply in_inPolySet; simpl in |- *; auto. red in |- *; intros H; inversion H. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)