proposition: Lemma normal_0notroot (p : {poly R}) : p \is normal -> ~~(root p 0) -> (forall k, (k < (size p).-1)%N -> 0 < p`_k).
proof: Proof. move=> Hpnormal H. rewrite normal_0notroot_b // in H. move/forallP : H => H k Hk. apply: (H (Ordinal Hk)). 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)