proposition: Lemma normal_coef_chain_1 (p : {poly R}) : ~~ root p 0 -> p \is normal -> forall k, (0 < k)%N -> forall i, p`_k.-1 * p`_(k.+1 +i) <= p`_(k + i) * p`_k .
proof: Proof. move=> Hp0notroot Hpnormal k Hk. have/normalP [H1 _ H3 _] := Hpnormal. elim => [ |i Hi ] //. rewrite !addn0 -expr2 H3 //. rewrite -subr_ge0. case Hik : (k + i.+1 < size p)%N. rewrite -(pmulr_lge0 (x:= p`_(k + i.+1))) //. rewrite mulrDl mulNr subr_ge0. apply: (le_trans (y:= p`_(k + i) * p`_k * p`_(k.+2 + i))). rewrite -[x in (x <= _)]mulrA [x in (_ * x)]mulrC !mulrA -!addSnnS -subr_ge0 -mulNr -mulrDl. case H : (p`_(k.+2 + i) == 0). by rewrite (eqP H) mulr0. by rewrite pmulr_lge0 ?subr_ge0 // lt_def H H1. have H := (H3 (k + i).+1 (ltn0Sn (k + i))). rewrite !addnS !addSn [x in (x * _)]mulrC [x in (_ <= x * _)]mulrC -subr_ge0 -!(mulrA p`_k) -mulrN -mulrDr mulrC pmulr_lge0. by rewrite subr_ge0 -expr2 //. apply: normal_0notroot => //. apply: (leq_ltn_trans (n:=(k + i))). by apply: leq_addr. by rewrite -subn1 ltn_subRL addnC addn1 -addnS. by apply normal_0notroot_2. have Hik2 : (k + i.+2 < size p)%N = false. apply: negbTE. rewrite -leqNgt. apply: (leq_trans (n := (k + i.+1))). by rewrite leqNgt Hik. by rewrite !addnS leqnSn. by rewrite addSnnS -{4}(coefK p) coef_poly //= Hik2 mulr0 oppr0 addr0 -{1}(coefK p) coef_poly Hik mul0r. 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)