proposition: Lemma nth_coeff_wd : forall n p p', p [=] p' -> nth_coeff n p [=] nth_coeff n p'.
proof: Proof. intros. generalize (fun_strext_imp_wd _ _ (nth_coeff n)); intro. unfold fun_wd in H0. apply H0. unfold fun_strext in |- *. intros. apply nth_coeff_strext with n. assumption. assumption. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings