proposition: Lemma normal_coef_geq0 (p : {poly R}) : p \is normal -> forall k, 0 <= p`_k.
proof: Proof. rewrite normalE; case: p=> s /= _. case: s=> // a []=> [Ha | b l]. by case=> [ | []] //; rewrite ltW. elim: l a b=> [a b /andP [Ha Hb] | c l IHl a b]. by case=> // [][]=> [ | []] //; rewrite ltW. case/andP=> H1 /orP H2 [] /=. rewrite le0r eq_sym. case: H2=> [-> | /andP [/andP [_ ->]]] //. by rewrite orbT. 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)