proposition: Lemma subp_all_pos : all_pos (mask (map (fun x => x != 0) (mid q)) (drop 1 p)).
proof: Proof. rewrite (@all_pos_subseq R _ (drop 1 p)) // ?all_pos_dropp//. apply/subseqP. exists [seq x != 0 | x <- mid (R:=R) q] => //. by rewrite size_map mid_size size_drop 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)