proposition: Lemma nth_coeff_minus : forall (p q : RX) i, nth_coeff i (p[-]q) [=] nth_coeff i p[-]nth_coeff i q.
proof: Proof. intros. astepl (nth_coeff i (p[+][--]q)). astepl (nth_coeff i p[+]nth_coeff i [--]q). Step_final (nth_coeff i p[+][--] (nth_coeff i q)). Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings