proposition: Lemma rootC_ge0 n x : (n > 0)%N -> (0 <= n.-root x) = (0 <= x).
proof: Proof. set y := n.-root x => n_gt0. apply/idP/idP=> [/(exprn_ge0 n) | x_ge0]; first by rewrite rootCK. rewrite -(ge_leif (leif_Re_Creal y)). have Ray: `|y| \is real by apply: normr_real. rewrite -(Creal_ReP _ Ray) rootC_Re_max ?(Creal_ImP _ Ray) //. by rewrite -normrX rootCK // ger0_norm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)