proposition: Lemma normal_root0 (p : {poly R}) : root p 0 -> forall k, (k < (\mu_0 p))%N -> p`_k = 0.
proof: Proof. move=> Hproot k Hkmu. have H := root_mu p 0. rewrite subr0 Pdiv.IdomainMonic.dvdp_eq in H. by rewrite (eqP H) coefMXn Hkmu. exact: monicXn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)