proposition: Lemma q_0_neq0 : q`_0 != 0.
proof: Proof. by rewrite negbT // lt_eqF // q_0_lt0. 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)