proposition: Lemma roots_on_uniq p a b s1 s2 : sorted <%R s1 -> sorted <%R s2 -> roots_on p `]a, b[ s1 -> roots_on p `]a, b[ s2 -> s1 = s2.
proof: Proof. wlog: s1 s2 / (size s1 <= size s2)%N => [hwlog ? ? ? ?|]. by case: (leqP (size s1) (size s2)) => [|/ltnW] /hwlog ->. elim: s1 p a b s2 => [| r1 s1 ih] p a b [| r2 s2] les12 ps1 ps2 rs1 rs2 //=. have rpr2 : root p r2 by apply: (roots_on_root rs2); rewrite mem_head. have abr2 : r2 \in `]a, b[ by apply: (roots_on_in rs2); rewrite mem_head. by have:= (rs1 r2); rewrite rpr2 !abr2 in_nil. have er1r2 : r1 = r2. move: (rs1 r2) (rs2 r1); rewrite rs2 rs1 !mem_head !in_cons //=. move=> /esym /predU1P [-> //|hr2] /esym /predU1P [-> //|hr1]. move/(order_path_min lt_trans)/allP/(_ r2 hr2): ps1 => h1. move/(order_path_min lt_trans)/allP/(_ r1 hr1)/(lt_trans h1): ps2. by rewrite ltxx. congr (_ :: _) => //; rewrite er1r2 in ps1 rs1. move: (roots_on_cons ps1 rs1) (roots_on_cons ps2 rs2). exact: ih (path_sorted ps1) (path_sorted ps2). 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)