proposition: Lemma normal_lead_coef_gt0 (p : {poly R}) : p \is normal -> 0 < lead_coef p.
proof: Proof. rewrite normalE lead_coefE; case: p=> s /= _. case: s=> // a [] => [Ha | b l] //. elim: l a b=> [a b /andP [Ha Hb]| c l IHl a b ] //. case/andP=> H1 /orP H2. exact: (IHl b c H1). 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)