proposition: Lemma normal_all_pos : forall (p : {poly R}), p \is normal -> ~~(root p 0) -> all_pos p.
proof: Proof. move=> p Hpnormal H0noroot; apply/all_posP. by apply: normal_0notroot_2. 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)