proposition: Lemma nth_coeff_complicated : forall a b (p : RX) n, nth_coeff (S n) ((_C_ a[*]_X_[+]_C_ b) [*]p) [=] a[*]nth_coeff n p[+]b[*]nth_coeff (S n) p.
proof: Proof. intros. astepl (nth_coeff (S n) (_C_ a[*]_X_[*]p[+]_C_ b[*]p)). astepl (nth_coeff (S n) (_C_ a[*]_X_[*]p) [+]nth_coeff (S n) (_C_ b[*]p)). astepl (nth_coeff (S n) (_C_ a[*] (_X_[*]p)) [+]b[*]nth_coeff (S n) p). astepl (a[*]nth_coeff (S n) (_X_[*]p) [+]b[*]nth_coeff (S n) p). algebra. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings