proposition: Lemma spseq_seqn0 : (mask (map (fun x => x != 0) (mid q)) spseq) = seqn0 spseq.
proof: Proof. by rewrite seqn0_as_mask 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)