proposition: Lemma prop_normal (p : {poly R}) : [/\ (forall k, 0 <= p`_k), (0 < lead_coef p), (forall k, (1 <= k)%N -> p`_(k.-1) * p`_(k.+1) <= (p`_k) ^+2) & (forall i, 0 < p`_i -> forall j, (i < j)%N -> (j < (size p).-1)%N -> 0 < p`_j)] -> p \is normal.
proof: Proof. case; rewrite normalE lead_coefE; case: p=> s /= _. case: s => [ | a [] // b l]; first by rewrite ltxx. elim: l a b=> [a b /(_ 0%N) /= -> -> //| c l IHl a b Hge0 Hlc H2 Hgt0]. apply/andP; split. apply: IHl=>[k||[] // k _|k Hk j Hj1 Hj2] //. + exact: (Hge0 k.+1). - exact: (H2 k.+2). + exact: (Hgt0 k.+1 Hk j.+1). have:= (Hge0 0%N); rewrite le_eqVlt /=. case/orP=> [-> //| Ha]. by rewrite (Hgt0 0%N Ha 1%N) // (H2 1%N) // Ha orbT. 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)