proposition: Lemma nth_coeff_mult : forall (p q : RX) n, nth_coeff n (p[*]q) [=] Sum 0 n (fun i => nth_coeff i p[*]nth_coeff (n - i) q).
proof: Proof. intro; induction p as [| s p Hrecp]. intros. stepl (nth_coeff n ([0]:RX)). simpl in |- *. apply eq_symmetric_unfolded. apply Sum_zero. auto with arith. intros. algebra. apply nth_coeff_wd. change ([0][=][0][*]q). algebra. intros. apply eq_transitive_unfolded with (nth_coeff n (_C_ s[*]q[+]_X_[*] ((p:RX) [*]q))). apply nth_coeff_wd. change ((s[+X*]p) [*]q [=] _C_ s[*]q[+]_X_[*] ((p:RX) [*]q)) in |- *. astepl ((_C_ s[+]_X_[*]p) [*]q). Step_final (_C_ s[*]q[+]_X_[*]p[*]q). astepl (nth_coeff n (_C_ s[*]q) [+]nth_coeff n (_X_[*] ((p:RX) [*]q))). astepl (s[*]nth_coeff n q[+]nth_coeff n (_X_[*] ((p:RX) [*]q))). induction n as [| n Hrecn]; intros. astepl (s[*]nth_coeff 0 q[+][0]). astepl (s[*]nth_coeff 0 q). astepl (nth_coeff 0 (cpoly_linear _ s p) [*]nth_coeff 0 q). pattern 0 at 2 in |- *. replace 0 with (0 - 0). apply eq_symmetric_unfolded. apply Sum_one with (f := fun i : nat => nth_coeff i (cpoly_linear _ s p) [*]nth_coeff (0 - i) q). auto. astepl (s[*]nth_coeff (S n) q[+]nth_coeff n ((p:RX) [*]q)). apply eq_transitive_unfolded with (nth_coeff 0 (cpoly_linear _ s p) [*]nth_coeff (S n - 0) q[+] Sum 1 (S n) (fun i : nat => nth_coeff i (cpoly_linear _ s p) [*]nth_coeff (S n - i) q)). apply bin_op_wd_unfolded. algebra. astepl (Sum 0 n (fun i : nat => nth_coeff i p[*]nth_coeff (n - i) q)). apply Sum_shift. intros. simpl in |- *. algebra. apply eq_symmetric_unfolded. apply Sum_first with (f := fun i : nat => nth_coeff i (cpoly_linear _ s p) [*]nth_coeff (S n - i) q). Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings