proposition: Lemma one_root2_uniq p a: one_root2 p a -> uniqueness (fun z => a < z /\ root p z).
proof: Proof. move => [pp]; set c:=pp.1; set k := pp.2. move => [/andP [ac kp] nii slk]. move => z1 z2 [az1 /eqP rz1][az2 /eqP rz2]. case: (lerP z1 c) => z1c. have aux: (a < z1 <= c) by rewrite az1 z1c. by move: (nii _ aux); rewrite rz1 ltxx. case: (lerP z2 c) => z2c. have aux: (a < z2 <= c) by rewrite az2 z2c. by move: (nii _ aux); rewrite rz2 ltxx. case /orP: (le_total z1 z2) => cp; apply/eqP; rewrite eq_le; apply/andP; split => //. have aux:(c <= z1 <= z2) by rewrite (ltW z1c) cp. move: (slk _ _ aux). by rewrite rz1 rz2 addrN (pmulr_rle0 _ kp) subr_le0. have aux:(c <= z2 <= z1) by rewrite (ltW z2c) cp. move: (slk _ _ aux). by rewrite rz1 rz2 addrN (pmulr_rle0 _ kp) subr_le0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol