proposition: Lemma prev_rootP (p : {poly R}) a b : prev_root_spec p a b (p.[prev_root p a b] == 0) (prev_root p a b).
proof: Proof. rewrite /prev_root /=; move hs: (roots _ _ _)=> s. case: (lastP s) hs=> {s} [|s x] hs /=. case: (eqVneq p 0) hs => [->|p0] hs. by rewrite hornerC eqxx; constructor. by constructor=> // y hy; apply: (roots_nil p0 hs). move/eqP: hs; rewrite last_rcons roots_rcons. case/and5P=> p0 hx /eqP rap rpx rx. rewrite (negPf p0) (rootPt rpx); constructor=> //; first by apply/eqP. by move=> y hy /=; move/(roots_nil p0): (rap); apply. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)