proposition: Lemma eq_algcreal_dec (x y : algcreal) : {(x == y)%CR} + {(x != y)%CR}.
proof: Proof. have /= [d_eq0|d_neq0] := algcreal_eq0_dec (sub_algcreal x y); [left|right]. apply: eq_crealP; exists_big_modulus m F. by move=> e i e_gt0 hi; rewrite (@eq0_modP _ _ d_eq0). by close. pose_big_enough i. apply: (@neq_crealP _ (lbound d_neq0) i i); do ?by rewrite ?lbound_gt0. by rewrite (@lbound0P _ _ d_neq0). by close. 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)