proposition: Theorem CombLinear_spoly : forall (Q : list (poly A0 eqA ltM)) (p q : list (Term A n)) (Cp : canonical A0 eqA ltM p) (Cq : canonical A0 eqA ltM q), inPolySet A A0 eqA n ltM p Q -> inPolySet A A0 eqA n ltM q Q -> CombLinear Q (spolyf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec p q Cp Cq).
proof: Proof. Proof using os cs. intros Q p; case p. simpl in |- *; auto. intros a l q; case q. simpl in |- *; auto. intros a0 l0 Cp Cq H' H'0. cut (canonical A0 eqA ltM l0); [ intros Op1 | apply canonical_imp_canonical with (a := a0) ]; auto. cut (canonical A0 eqA ltM l); [ intros Op2 | apply canonical_imp_canonical with (a := a) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a); [ intros nZa | apply (canonical_nzeroP A A0 eqA n ltM) with (p := l); auto ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) a0); [ intros nZa0 | apply (canonical_nzeroP A A0 eqA n ltM) with (p := l0); auto ]. apply CombLinear_comp with (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) a a0) (b:=a) nZa) (pX a l)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a a0) (b:=a0) nZa0) (pX a0 l0))); 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 a l) (pX a0 l0) Cp Cq) (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) a a0) (b:=a) nZa) (pX a l)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a a0) (b:=a0) nZa0) (pX a0 l0)))) in |- *. apply spoly_is_minus with (1 := cs); auto. Qed.