proposition: Lemma normal_0notroot_b (p : {poly R}) : p \is normal -> (~~(root p 0) = [forall k : 'I_((size p).-1), 0 < p`_k]).
proof: Proof. move=> Hpnormal. have/normalP [H1 _ _ H4] := Hpnormal. have Hp := (normal_neq0 Hpnormal). apply/idP/idP. move/rootPf=> H. rewrite horner_coef0 in H. have Hp0 : 0 < p`_0 by rewrite lt_def H (H1 0%N). apply/forallP; case; case=> [ | n Hn] //. by apply: (H4 0%N Hp0 n.+1 (ltn0Sn n) Hn). apply: contraL => /rootPt Hproot0. rewrite negb_forall; apply/existsP. have H0 : (0 < (size p).-1)%N. rewrite -subn1 -(ltn_add2r 1) !addn1 subn1 prednK. rewrite (root_size_gt1 (a:=0)) //. rewrite (ltn_trans (n:= 1)) //. rewrite (root_size_gt1 (a:=0)) //. exists (Ordinal H0). rewrite -leNgt le_eqVlt. apply/orP; left. by rewrite horner_coef0 in Hproot0. 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)