proposition: Lemma q_size : d = (size p).+1 .
proof: Proof. have Hpneq0 := (normal_neq0 Hpnormal). rewrite mulrDr size_addl. by rewrite size_mulX. rewrite mulrC -polyCN mul_polyC size_mulX //. by rewrite (@leq_ltn_trans (size p)) // size_scale_leq. 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)