proposition: Lemma mid_cons (s : seq R) (a : R) : mid (a :: s) = take (size s).-1 s.
proof: Proof. by rewrite mid_2 /= 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)