proposition: Lemma fpx_resp_coef : forall (f:zx)(n:nat), (zfp (nth_coeff n f)) [=] (nth_coeff n (zxfpx f)).
proof: Proof. induction f. intuition. induction n. intuition. astepl (zfp (nth_coeff n f)). astepr (nth_coeff n (zxfpx f)). apply (IHf n). Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree