proposition: Lemma normal_squares (p : {poly R}) : p \is normal -> (forall k, (1 <= k)%N -> p`_(k.-1) * p`_(k.+1) <= p`_k ^+2).
proof: Proof. rewrite normalE; case: p=> s /= _. case: s=> // a [] => [Ha [] // n Hn | b l] //. by rewrite mulr0; apply: sqr_ge0. elim: l a b => [a b /andP [Ha Hb] | c l IHl a b]. by case=> // [][] => [_ | n _]; rewrite mulr0; apply: sqr_ge0. case/andP=> H1 /orP H2 [] // [] => [_ | n Hn]. case: H2=> [/eqP <-|/andP [] /andP [] H2 _ _] //. by rewrite mul0r; apply: sqr_ge0. exact: (IHl b c H1 n.+1). 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)