proposition: Lemma algcreal_eq0_dec (x : algcreal) : {(x == 0)%CR} + {(x != 0)%CR}.
proof: Proof. pose p := annul_creal x; move: {2}(size _)%N (leqnn (size p))=> n. elim: n x @p => [x p|n ihn x p le_sp_Sn]. by rewrite leqn0 size_poly_eq0 /p annul_creal_eq0. move: le_sp_Sn; rewrite leq_eqVlt; have [|//|eq_sp_Sn _] := ltngtP. by rewrite ltnS=> /ihn ihnp _; apply: ihnp. have px0 : (p.[x] == 0)%CR by apply: root_annul_creal. have [cpX|ncpX] := boolP (coprimep p 'X). by right; move: (cpX)=> /coprimep_root /(_ px0); rewrite horner_crealX. have [eq_pX|] := altP (p =P 'X). by left; move: px0; rewrite eq_pX horner_crealX. rewrite -eqp_monic /p ?monicX // negb_and orbC. have:= ncpX; rewrite coprimepX -dvdp_XsubCl subr0 => /negPf-> /= ndiv_pX. have [r] := smaller_factor (monic_annul_creal _) px0 ndiv_pX ncpX. rewrite eq_sp_Sn ltnS => /andP[le_r_n monic_r] rx_eq0. exact: (ihn (AlgCReal monic_r rx_eq0)). 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)