proposition: Lemma all_pos_subseq : forall (s1 s2 : seq R), (all_pos s2) -> (subseq s1 s2) -> (all_pos s1).
proof: Proof. move=> s1 s2 /allP Hs2 /mem_subseq Hsubseq; by apply/allP=> y /Hsubseq /Hs2 Hy. 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)