proposition: Lemma pos_split1 p (s := pos_roots p) (q:= pos_cofactor p): p != 0 -> [/\ fact_list p s q, (forall x, 0 <x -> ~~ root q x) & q != 0].
proof: Proof. move => h; rewrite /s/q /pos_roots / pos_cofactor. move: (poly_split_fact p) => H; move: (s2valP' H) (s2valP H) => [h1 _] h2. split => //; first by apply: h1. by apply/eqP => qz; move:h2 => [] pv; move: h; rewrite {1} pv qz mulr0 eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)