proposition: Lemma nth_coeff_ap_zero_imp : forall (p : RX) n, nth_coeff n p [#] [0] -> p [#] [0].
proof: Proof. intros. cut (nth_coeff n p [#] nth_coeff n [0]). intro H0. apply (nth_coeff_strext _ _ _ _ H0). algebra. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings