proposition: Lemma next_rootP (p : {poly R}) a b : next_root_spec p a b (p.[next_root p a b] == 0) (next_root p a b).
proof: Proof. rewrite /next_root /=; case hs: roots => [|x s] /=. 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 roots_cons; case/and5P=> p0 hx /eqP rap rpx rx. rewrite (negPf p0) (rootPt rpx); constructor=> //; first by apply/eqP. by move=> y hy; apply: (roots_nil p0 rap). 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)