proposition: Lemma root_seq_poly_pos x s : (forall p , p \in s -> p !=0) -> x \in root_seq_poly s -> (0 < x.2)%N.
proof: Proof. elim : s=> [|p l IHl H]; first by rewrite in_nil. rewrite mem_cat. case/orP; first by apply: root_mu_seq_pos; apply: H; rewrite mem_head. by apply: IHl=> q Hq; apply: H; rewrite in_cons Hq orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)