proposition: Lemma normal_coef_chain_2 (p : {poly R}) : ~~ root p 0 -> p \is normal -> forall k, (0 < k)%N -> forall i, (k <= i)%N -> p`_k.-1 * p`_(i.+1) <= p`_i * p`_k .
proof: Proof. move=> Hp0notroot Hpnormal k Hk i Hi. have H := (normal_coef_chain_1 Hp0notroot Hpnormal Hk (i - k)). by rewrite !addnBA // addnC (addnC k i) -addnBA // subSnn addn1 addnK in H. 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)