proposition: Fact rootC_subproof n x : rootC_spec n x.
proof: Proof. have realRe2 u : Re2 u \is Num.real by rewrite realEsqr expr2 {2}/Re2 -{2}[u]conjCK addrC -rmorphD -normCK exprn_ge0. have argCle_total : total argCle. move=> u v; rewrite /total /argCle. by do 2!case: (nnegIm _) => //; rewrite ?orbT //= real_leVge. have argCle_trans : transitive argCle. move=> u v w /implyP geZuv /implyP geZvw; apply/implyP. by case/geZvw/andP=> /geZuv/andP[-> geRuv] /le_trans->. pose p := 'X^n - (x *+ (n > 0))%:P; have [r0 Dp] := closed_field_poly_normal p. have sz_p: size p = n.+1. rewrite size_addl ?size_polyXn // ltnS size_opp size_polyC mulrn_eq0. by case: posnP => //; case: negP. pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted. have{} Dp: p = \prod_(z <- r) ('X - z%:P). rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb. by rewrite subr0 eqxx scale1r; apply/esym/perm_big; rewrite perm_sort. have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r). move=> n_gt0; rewrite -root_prod_XsubC -Dp rootE !hornerE n_gt0. by rewrite subr_eq0; apply: eqP. exists r`_0 => [|z n_gt0 /(mem_rP z n_gt0) r_z]. have sz_r: size r = n by apply: succn_inj; rewrite -sz_p Dp size_prod_XsubC. case: posnP => [n0 | n_gt0]; first by rewrite nth_default // sz_r n0. by apply/mem_rP=> //; rewrite mem_nth ?sz_r. case: {Dp mem_rP}r r_z r_arg => // y r1 /[1!inE] /predU1P[-> _|r1z]. by apply/implyP=> ->; rewrite lexx. by move/(order_path_min argCle_trans)/allP->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)