proposition: Lemma itv_roots (p :{poly R}) (a b : R) : {s : seq R & roots_spec p (topred `]a, b[) s p (p == 0) s}.
proof: Proof. elim: (size p) {-2}p (leqnn (size p)) a b => {p} [|n ihn] p sp a b. by move/size_poly_leq0P: sp => ->; rewrite eqxx; exists [::]; constructor. case: eqVneq => [->|p0]; first by exists [::]; constructor. case: (boolP (p^`() == 0)) => [|p'0]. rewrite -derivn1 -derivn_poly0 => /size1_polyC pC; exists [::]. by constructor=> // x; rewrite pC rootC -polyC_eq0 -pC (negPf p0) andbF. have {}/ihn /(_ a b) [sp'] : (size p^`() <= n)%N. rewrite -ltnS; apply: leq_trans sp; rewrite size_deriv prednK // lt0n. by rewrite size_poly_eq0 p0. elim: sp' a => [|r1 sp' hsp'] a hp'. case: hp' p'0 => //= p'0 /roots_on_nil /monotonic_rootN [h| [r rh]] _ _. by exists [::]; constructor. by exists [:: r]; constructor; rewrite //= andbT. case: hp' p'0 => //= p'0 hroots' hpath' _. case: (min_roots_on _ hroots') => [|hr1 har1 p'r10 hr1b]. by rewrite order_path_min //; apply: lt_trans. case: (hsp' r1) p0 => [|s]. by rewrite (negPf p'0); constructor; rewrite // (path_sorted hpath'). case; rewrite ?eqxx // => p0 hroot hsort _. move/monotonic_rootN: (roots_on_nil har1). case pr1 : (root p r1); case => hrootsl; last 2 first. - exists s; constructor=> //. by rewrite -[s]cat0s; apply: (cat_roots_on hr1); rewrite // pr1. - case: hrootsl=> r hr; exists (r::s); constructor=> //=. by rewrite -cat1s; apply: (cat_roots_on hr1); rewrite // pr1. rewrite path_min_sorted //; apply/allP=> y; rewrite -hroot; case/andP=> hy _. rewrite (lt_trans (_ : _ < r1)) ?(itvP hy) //. by rewrite (itvP (roots_on_in hr (mem_head _ _))). - exists (r1::s); constructor=> //=; last first. rewrite path_min_sorted //; apply/allP => y; rewrite -hroot. by case/andP => /itvP->. move=> x; rewrite in_cons; have [->|exr1] /= := eqVneq; first by rewrite hr1. rewrite -hroot (itv_splitUeq hr1) (negPf exr1) /=. case: (_ \in `]r1, _[); rewrite (orbT, orbF); [by []|]. by apply: contraFF (hrootsl x) => ->. - case: hrootsl => r0 /min_roots_on [] // hr0 har0 pr0 hr0r1. exists [:: r0, r1 & s]; constructor=> //=; last first. rewrite (itvP hr0) /= path_min_sorted //; apply/allP=> y. by rewrite -hroot; case/andP => /itvP ->. move=> y; rewrite !in_cons (itv_splitUeq hr1) (itv_splitUeq hr0). have [->|eyr0] := eqVneq y r0; rewrite ?orbT ?pr0 //=. have [->|eyr1] := eqVneq y r1; rewrite ?orbT ?pr1 //=. move: (hr0r1 y) (har0 y); rewrite -!hroot. case: (_ \in `]r0, r1[) => /= [->|_]; rewrite ?andbF ?orbF //. by case: (_ \in `]a, r0[) => /= [->|_]; rewrite ?andbF. 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)