proposition: Lemma nth_coeff_plus : forall (p q : RX) n, nth_coeff n (p[+]q) [=] nth_coeff n p[+]nth_coeff n q.
proof: Proof. do 2 intro. pattern p, q in |- *. apply poly_double_comp_ind. intros. astepl (nth_coeff n (p1[+]q1)). astepr (nth_coeff n p1[+]nth_coeff n q1). apply H1. intros. simpl in |- *. algebra. intros. elim n. simpl in |- *. algebra. intros. astepl (nth_coeff n0 (p0[+]q0)). generalize (H n0); intro. astepl (nth_coeff n0 p0[+]nth_coeff n0 q0). algebra. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings