fact: Definition AlgCRealOf (p : {poly F}) (x : creal F) (p_neq0 : p != 0) (px_eq0 : (p.[x] == 0)%CR) := AlgCReal (monic_monic_from_neq0 p_neq0) (root_monic_from_neq0 px_eq0).
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)