proposition: Lemma q_n : q`_d.-1 = p`_(d.-2).
proof: Proof. rewrite -p_size mulrDr coefD -polyCN (mulrC p ((-a)%:P)) mul_polyC coefZ. rewrite coefMX. have H : (((size p) == 0%N) = false). rewrite size_poly_eq0. apply/eqP/eqP. by apply: normal_neq0. by rewrite H /= {H} -{3}(coefK p) coef_poly ltnn mulr0 addr0. 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)