fact: Definition div_algcreal (x y : algcreal) := match eq_algcreal_dec y (cst_algcreal 0) with | left y_eq0 => cst_algcreal 0 | right y_neq0 => let: exist2 y' py'0_neq0 (y'_neq0, _) := simplify_algcreal y_neq0 in AlgCRealOf (div_annihilant_algcreal_neq0 x py'0_neq0) (@root_div_algcreal x y' y'_neq0 py'0_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)