proposition: Fact closedFieldAxiom : GRing.closed_field_axiom type.
proof: Proof. move=> n a n_gt0; pose p := 'X^n - \poly_(i < n) CtoL (a i). have Ap: {in p : seq L, integralRange QtoL}. move=> _ /(nthP 0)[j _ <-]; rewrite coefB coefXn coef_poly. apply: integral_sub; first exact: integral_nat. by case: ifP => _; [apply: CtoL_P | apply: integral0]. have sz_p: size p = n.+1. by rewrite size_addl size_polyXn // size_opp ltnS size_poly. have [z pz0]: exists z, root p z by apply/closed_rootP; rewrite sz_p eqSS -lt0n. have Az: integralOver ratr z. by apply: integral_root Ap; rewrite // -size_poly_gt0 sz_p. exists (LtoC Az); apply/CtoL_inj; rewrite -[CtoL _]subr0 -(rootP pz0). rewrite rmorphXn /= LtoC_K hornerD hornerXn hornerN opprD addNKr opprK. rewrite horner_poly rmorph_sum; apply: eq_bigr => k _. by rewrite rmorphM rmorphXn /= LtoC_K. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path bigop finset prime order ssralg) mathcomp(poly polydiv mxpoly generic_quotient countalg) mathcomp(ssrnum closed_field ssrint archimedean rat intdiv) mathcomp(algebraics_fundamentals)