proposition: Lemma ivt (p : {poly (alg F)}) (a b : alg F) : a <= b -> p.[a] <= 0 <= p.[b] -> exists2 x : alg F, a <= x <= b & root p x.
proof: Proof. move=> le_ab hp; have [x /andP [hax hxb]] := @weak_ivt _ _ _ _ le_ab hp. rewrite -[x]from_algK fmorph_root=> rpx; exists (from_alg x)=> //. by rewrite -ler_to_alg from_algK hax -ler_to_alg from_algK. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)