proposition: Lemma mid_2 : forall (s : seq R), mid s = (take (size s).-2 (drop 1 s)).
proof: Proof. elim=> [ |a l IHl ] //=. case: l IHl => [ |b l IHbl ] //. rewrite drop0 /mid. have Hsize : ((size [::a, b & l]).-1 = (size (b :: l)).-1.+1). by rewrite prednK. by rewrite Hsize /= drop0. 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)