proposition: Lemma poly_at_zero : forall p : RX, p ! [0] [=] nth_coeff 0 p.
proof: Proof. intros. induction p as [| s p Hrecp]; intros. simpl in |- *. algebra. simpl in |- *. Step_final (s[+][0]). Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings