proposition: Lemma mid_coef_2 (s : seq R) k: (0%N < k)%N -> (k < (size s).-1)%N -> (mid s)`_k.-1 = s`_k.
proof: Proof. move=> Hk1 Hk2. by rewrite mid_coef_1 prednK // mid_size -(@prednK k) // -(@ltn_add2r 1%N) !addn1 !prednK // (@ltn_trans k). 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)