proposition: Lemma ivt_sign (p : {poly R}) (a b : R) : a <= b -> sgr p.[a] * sgr p.[b] = -1 -> { x : R | x \in `]a, b[ & root p x}.
proof: Proof. move=> hab /eqP; rewrite mulrC mulr_sg_eqN1=> /andP [spb0 /eqP spb]. case: (@poly_ivt (sgr p.[b] *: p) a b) => //. by rewrite in_itv /= !hornerZ {1}spb mulNr -!normrEsg oppr_cp0 !normrE. move=> c hc; rewrite rootZ ?sgr_eq0 // => rpc; exists c=> //. rewrite !in_itv /= !lt_neqAle andbACA [(_ <= _) && _]hc andbT eq_sym -negb_or. apply: contraL rpc => /orP [] /eqP ->; rewrite /root ?(negPf spb0) //. by rewrite -sgr_cp0 -[sgr _]opprK -spb eqr_oppLR oppr0 sgr_cp0. 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)