proposition: Lemma seqn0q_size : (1 < size (seqn0 q))%N.
proof: Proof. by rewrite seqn0_size_2 // ?q_0_lt0 // ?q_n_gt0. 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)