proposition: Theorem Cb_sp : forall (a b : poly A0 eqA ltM) (Q : list (poly A0 eqA ltM)), Cb a Q -> Cb b Q -> Cb (spolyp a b) Q.
proof: Proof. intros a b; case a; case b; simpl in |- *; auto. intros x; case x; auto. intros a0 l H' x0; case x0; auto. intros a1 l0 H'0 Q H'1 H'2. cut (~ zeroP (A:=A) A0 eqA (n:=n) a0); [ intros Z0 | apply canonical_nzeroP with (ltM := ltM) (p := l); auto ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) a1); [ intros Z1 | apply canonical_nzeroP with (ltM := ltM) (p := l0); auto ]. apply CombLinear_comp with (1 := cs) (p := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a0 a1) (b:=a0) Z0) (pX a0 l)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a0 a1) (b:=a1) Z1) (pX a1 l0))); auto. apply CombLinear_minuspf with (1 := cs); auto. apply CombLinear_mults1 with (1 := cs); auto. apply CombLinear_mults1 with (1 := cs); auto. apply spolyf_canonical with (1 := cs); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. change (eqP A eqA n (spolyf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec (pX a0 l) (pX a1 l0) H' H'0) (minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a0 a1) (b:=a0) Z0) (pX a0 l)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a0 a1) (b:=a1) Z1) (pX a1 l0)))) in |- *. apply spoly_is_minus with (1 := cs); auto. Qed.
imports: Buchberger(moreCoefStructure)