proposition: Lemma Abs_poly_nth_coeff : forall P i, nth_coeff i (AbsPoly P) [=] AbsIR (nth_coeff i P).
proof: Proof. intro P. pattern P; apply Ccpoly_induc; clear P. intro; rewrite -> AbsPoly_zero, nth_coeff_zero. symmetry; apply AbsIRz_isz. intros P c Hrec n. rewrite AbsPoly_linear. destruct n. rewrite -> coeff_O_lin; reflexivity. rewrite -> coeff_Sm_lin. rewrite -> Hrec. apply AbsIR_wd. symmetry; apply coeff_Sm_lin. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots