fact: Definition inv_algcreal (x : algcreal) := match eq_algcreal_dec x (cst_algcreal 0) with | left x_eq0 => cst_algcreal 0 | right x_neq0 => AlgCReal (@monic_annul_creal _) (@root_inv_algcreal _ x_neq0) 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)