proposition: Lemma p_size : size p = d.-1.
proof: Proof. by rewrite (@pred_Sn (size p)) q_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)