proposition: Lemma q_0 : q`_0 = -a * p`_0.
proof: Proof. rewrite mulrDr coefD -polyCN (mulrC p ((-a)%:P)) mul_polyC coefZ polyseqMX. by rewrite add0r. by apply: normal_neq0. 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)