proposition: Lemma spseq_increasing : increasing spseq.
proof: Proof. have/normalP [_ _ H3 _] := Hpnormal. apply/increasingP => k Hk. rewrite spseq_size in Hk. rewrite (@spseq_coef k) //. rewrite (@spseq_coef k.+1) //. rewrite ler_sub // ler_pdivr_mulr. rewrite mulrC mulrA ler_pdivl_mulr. by rewrite -expr2 (H3 k.+1). rewrite (normal_0notroot_2 Hpnormal Hp0noroot) //. by rewrite -(@addn2 k) addnC -ltn_subRL p_size subn2. rewrite (normal_0notroot Hpnormal Hp0noroot) //. by rewrite -(@addn1 k) addnC -ltn_subRL p_size -subn2 -subnDA addnC subnDA subn2 subn1. by rewrite -(@addn1 k) addnC -ltn_subRL -subn2 -subnDA addnC subnDA subn2 subn1. by rewrite (leq_trans Hk) // -(@subn2 (size q)) -subn1 leq_subLR addnC addn1. 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)