proposition: Lemma minn_seqn0spseq_maskdropp : (minn (size (seqn0 spseq)) (size (mask [seq x != 0 | x <- mid (R:=R) q] (drop 1 p)))) = (size (seqn0 spseq)).
proof: Proof. by rewrite -size_seqn0spseq_maskdropp minnE subKn. 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)