proposition: Lemma is_next_root p a b x : next_root_spec p a b (root p x) x -> x = next_root p a b.
proof: Proof. case; first by move->; rewrite /next_root eqxx. move=> y; case: next_rootP; first by move->; rewrite eqxx. move=> y' np0 py'0 hy' hp' _ py0 hy hp. wlog: y y' hy' hy hp' hp py0 py'0 / y <= y'. by case/orP: (le_total y y')=> lyy' hw; [|symmetry]; apply: hw. case: ltrgtP=> // hyy' _; move: (hp' y). by rewrite in_itv /= (itvP hy) hyy' rootE py0 eqxx; move/(_ isT). move=> c p0 ->; case: leP => hba; first by rewrite itv_ge // -leNgt. by move=> hpz _ py0 /hpz; rewrite rootE py0 eqxx. case: next_rootP; first by move->; rewrite eqxx. by move=> y np0 py0 hy _ c _ _ /(_ _ hy); rewrite rootE py0 eqxx. by move=> c _ -> _ c' _ ->. 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)