proposition: Lemma mid_seqn0q_size : size (mid (seqn0 q)) = size (seqn0 spseq).
proof: Proof. by rewrite mid_seqn0_C ?q_0_neq0 // ?q_n_neq0 // !seqn0_as_mask !size_mask ?size_map // map_midq_spseq. 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)