proposition: Lemma all_neq0P (s : seq R) : reflect (forall k, (k < size s)%N -> s`_k != 0) (all_neq0 s).
proof: Proof. by apply/all_nthP. 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)