proposition: Lemma one_root1_uniq p a b: one_root1 p a b -> uniqueness (fun z => a < z < b /\ root p z).
proof: Proof. move => [c [d [k [leqs pa nb dab]]]]. move => z1 z2 [/andP [z1a z1b] /eqP rz1] [/andP [z2a z2b] /eqP rz2]. move: leqs => /and4P [ac cd db k0]. case: (lerP z1 c) => z1c. have aux:(a < z1 <= c) by rewrite z1a z1c. by move: (pa z1 aux); rewrite rz1 ltxx. case: (lerP z2 c) => z2c. have aux:(a < z2 <= c) by rewrite z2a z2c. by move: (pa z2 aux); rewrite rz2 ltxx. case: (lerP z1 d) => z1d; last first. have aux: (d < z1 < b) by rewrite z1d z1b. by move: (nb z1 aux); rewrite rz1 ltxx. case: (lerP z2 d) => z2d; last first. have aux: (d < z2 < b) by rewrite z2d z2b. by move: (nb z2 aux); rewrite rz2 ltxx. case /orP: (le_total z1 z2) => cp. apply/eqP; rewrite eq_le; apply/andP; split => //. move: (dab _ _ (ltW z1c) cp z2d). by rewrite rz1 rz2 addrN (pmulr_rle0 _ k0) subr_le0. move: (dab _ _ (ltW z2c) cp z1d). rewrite rz1 rz2 addrN (pmulr_rle0 _ k0) subr_le0. move=> z1z2. by apply/eqP; rewrite eq_le cp z1z2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol