fact: Fixpoint to_algcreal_of (p : {poly F}) (c r : F) (i : nat) : F := match i with | 0 => c | i.+1 => let c' := to_algcreal_of p c r i in if p.[c' - r / 2%:R ^+ i] * p.[c'] <= 0 then c' - r / 2%:R ^+ i.+1 else c' + r / 2%:R ^+ i.+1 end.
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)