proposition: Lemma size_seqn0spseq_maskdropp : size (seqn0 spseq) = size (mask [seq x != 0 | x <- mid q] (drop 1 p)).
proof: Proof. rewrite -mid_seqn0q_size mid_seqn0_C ?q_0_neq0 // ?q_n_neq0 // seqn0_as_mask !size_mask //. by rewrite size_map. by rewrite size_map size_drop mid_size p_size subn1. 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)