proposition: Lemma spseq_coef k : (k < d.-2)%N -> spseq`_k = p`_k / p`_k.+1 - a.
proof: Proof. move=> Hk. have H : minn (size p) ((size p) - 1%N) = ((size p) - 1%N)%N. rewrite minnE subKn // subn1 -{2}(@prednK (size p)). by rewrite leqnSn. by rewrite ltnNge leqn0 size_poly_eq0 normal_neq0. rewrite /spseq (@nth_map _ 0). rewrite nth_zip_cond /= size_zip !size_drop H subn1 p_size Hk /=. by rewrite !nth_drop (addnC 1%N) addn1. by rewrite size_zip !size_drop H subn1 p_size. 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)