proposition: Lemma q_k k : (0%N < k)%N -> (k < d.-1)%N -> q`_k = (p`_k.-1/p`_k - a) * p`_k.
proof: Proof. move=> Hk1 Hk2. rewrite mulrDr coefD -polyCN (mulrC p ((-a)%:P)) mul_polyC coefZ coefMX. have H : ((k==0%N) = false). apply/eqP/eqP. by rewrite -lt0n. by rewrite H /= mulrDl divrK // unitf_gt0 // normal_0notroot_2 // 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)