proposition: Lemma seqn0q_1 : (1 < (size (seqn0 q)).-1)%N -> (seqn0 q)`_1 = (mid (seqn0 q))`_0.
proof: Proof. by move=> Hk; rewrite -{1}[(seqn0 q)`_1]mid_coef_2. 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)