proposition: Lemma all_pos_dropp : all_pos (drop 1 p).
proof: Proof. apply/all_posP => k Hk. rewrite nth_drop addnC addn1. apply/all_posP. by apply: normal_all_pos. rewrite size_drop in Hk. by rewrite -(@addn1 k) addnC -ltn_subRL. 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)