proposition: Lemma normal_some_coef_gt0 (p : {poly R}) : p \is normal -> forall i, 0 < p`_i -> forall j, (i < j)%N -> (j < (size p).-1)%N -> 0 < p`_j.
proof: Proof. rewrite normalE; case: p=> s /= _. case: s=> // a []=> [Ha [] // | b l] //. elim: l a b => [a b /andP [Ha Hb] | c l IHl a b]. by case=> // [_ |] [] // => [_|] [] // => [_|n _][]. case/andP =>H1 H2 [] => [Ha | i Hi] [] // => [|j Hj1 Hj2]. rewrite (lt_eqF Ha) /= in H2. have/andP [_ Hb] := H2. case=> // j _ Hj; first exact: (IHl b c H1 0%N Hb j.+1). exact: (IHl b c H1 i Hi). 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)