proposition: Lemma mid_seqn0q_decomp : mid (seqn0 q) = seqmul (seqn0 spseq) (mask (map (fun x => x != 0) (mid q)) (drop 1 p)).
proof: Proof. by rewrite mid_seqn0_C ?q_0_neq0 // ?q_n_neq0 // {1}seqmul_spseq_dropp {1}seqn0_as_mask mask_seqmul -spseq_seqn0 seqmul_spseq_dropp. 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)