proposition: Lemma mid_size : forall (s : seq R), size (mid s) = (size s).-2.
proof: Proof. elim => [|a l IHl] => //=. by rewrite /mid size_drop size_takel //= subn1. 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)