proposition: Lemma all_posP (s : seq R) : reflect (forall k, (k < size s)%N -> 0 < s`_k) (all_pos s).
proof: Proof. exact/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)