proposition: Lemma normal_0notroot_2 (p : {poly R}) : p \is normal -> ~~ root p 0 -> forall k, (k < (size p))%N -> 0 < p`_k.
proof: Proof. move=> Hpnormal H k Hk. have/normalP [_ H2 _ _] := Hpnormal. case Hk2 : (k < (size p).-1)%N. by apply: normal_0notroot. have Hk3 : (k == (size p).-1). rewrite eqn_leq. apply/andP; split. rewrite -ltnS prednK // size_poly_gt0. by apply: normal_neq0. by rewrite leqNgt Hk2. by rewrite (eqP Hk3) -lead_coefE. 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)