proposition: Lemma simplify_algcreal (x : algcreal) (x_neq0 : (x != 0)%CR) : {y | ((annul_creal y).[0] != 0) & ((y != 0)%CR * (x == y)%CR)%type}.
proof: Proof. elim: size {-3}x x_neq0 (leqnn (size (annul_creal x))) => {x} [|n ihn] x x_neq0 hx. by move: hx; rewrite leqn0 size_poly_eq0 annul_creal_eq0. have [dvdX|ndvdX] := boolP ('X %| annul_creal x); last first. by exists x=> //; rewrite -rootE -dvdp_XsubCl subr0. have monic_p: @annul_creal x %/ 'X \is monic. by rewrite -(monicMr _ (@monicX _)) divpK //. have root_p: ((@annul_creal x %/ 'X).[x] == 0)%CR. have := @eq_creal_refl _ ((annul_creal x).[x])%CR. rewrite -{1}(divpK dvdX) horner_crealM // root_annul_creal. by case/poly_mul_creal_eq0=> //; rewrite horner_crealX. have [//|/=|y *] := ihn (AlgCReal monic_p root_p); last by exists y. by rewrite size_divp ?size_polyX ?polyX_eq0 ?leq_subLR ?add1n. 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)