proposition: Lemma is_prev_root p a b x : prev_root_spec p a b (root p x) x -> x = prev_root p a b.
proof: Proof. case; first by move->; rewrite /prev_root eqxx. move=> y; case: prev_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/implyP: (hp y'). by rewrite rootE py'0 eqxx in_itv /= (itvP hy') hyy'. by move=> c _ _ hpz _ py0 /hpz; rewrite rootE py0 eqxx. case: prev_rootP=> //; first by move->; rewrite eqxx. move=> y ? py0 hy _ c _ ->. case: ltP hy=> hab; last by rewrite itv_ge // -leNgt. by move=> hy /(_ _ 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)