proposition: Lemma q_n_gt0 : (0 < q`_d.-1).
proof: Proof. rewrite q_n -p_size // -lead_coefE. by have/normalP [_ H _ _] := Hpnormal. 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)