proposition: Lemma q_0_lt0 : q`_0 < 0.
proof: Proof. rewrite q_0 // mulNr oppr_lt0 pmulr_rgt0 //. case : (ltnP 1%N (size p)) => Hpsize. apply: (@normal_0notroot _ _ Hpnormal Hp0noroot). rewrite -(ltn_add2r 1) !addn1 prednK ?Hpsize //. by apply: (@ltn_trans 1%N). rewrite normal_size_le1 // in Hpsize. rewrite (pred_Sn 0) -(eqP Hpsize) -lead_coefE. by have/normalP [_ H _ _] := Hpnormal. 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)