proposition: Lemma mid_seqn0_C : forall (s : seq R), (s`_0 != 0) -> (s`_(size s).-1 != 0) -> mid (seqn0 s) = seqn0 (mid s).
proof: Proof. elim => [ |a] //. case => [_ Ha _ |b l Hbl Ha Hln] //=. by rewrite Ha /mid /=. rewrite Ha /mid -drop1_seqn0_C // -take1_seqn0_C //. have H : ((size (a :: (if b != 0 then b :: seqn0 l else seqn0 l))).-1 = (size (seqn0 (b :: l))).-1.+1). by rewrite prednK // seqn0_size. by rewrite H take_cons /= drop0 Ha H take_cons /= 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)