proposition: Lemma seqn0q_n : (0 < (size (seqn0 q)).-2)%N -> (seqn0 q)`_(size (seqn0 q)).-2 = (mid (seqn0 q))`_((size (mid (seqn0 q))).-1)%N.
proof: Proof. move=> Hsize_2. have Hsize_1 : (0 < (size (seqn0 q)).-1)%N. rewrite -subn1 ltn_subRL addn0 in Hsize_2. by rewrite (ltn_trans _ Hsize_2). have Hsize : (0 < size (seqn0 q))%N. rewrite -subn1 ltn_subRL addn0 in Hsize_1. by rewrite (ltn_trans _ Hsize_1). rewrite mid_coef_2 mid_size //. by rewrite -(subn1 (size (seqn0 q))) ltn_subRL addnC addn1 subn1 prednK // {2}(pred_Sn (size (seqn0 q))) -(subn1 (size (seqn0 q)).+1) ltn_subRL addnC addn1 prednK. 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)