proposition: Lemma mid_coef_1 (s : seq R) k : (k < size (mid s))%N -> (mid s)`_k = s`_k.+1.
proof: Proof. move=> Hk. rewrite /mid nth_drop addnC addn1 nth_take //. by rewrite -(@addn1 k) addnC -ltn_subRL subn1 -mid_size. 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)