proposition: Lemma nth_coeff_zx2qx : forall P n, nth_coeff n (zx2qx P) [=] nth_coeff n P.
proof: Proof. intro P; pattern P; apply Ccpoly_induc; clear P. reflexivity. intros P c Hrec n. rewrite zx2qx_linear. induction n. reflexivity. rewrite -> coeff_Sm_lin, coeff_Sm_lin. apply Hrec. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg