proposition: Lemma rootC_lt0 n x : (1 < n)%N -> (n.-root x < 0) = false.
proof: Proof. set y := n.-root x => n_gt1; have n_gt0 := ltnW n_gt1. apply: negbTE; apply: wlog_neg => /negbNE lt0y; rewrite le_gtF //. have Rx: x \is real by rewrite -[x](rootCK n_gt0) rpredX // ltr0_real. have Re_y: 'Re y = y by apply/Creal_ReP; rewrite ltr0_real. have [z zn_x leR0z]: exists2 z, z ^+ n = x & 'Re z >= 0. have [w wn1 ltRw0] := neg_unity_root n_gt1. exists (w * y); first by rewrite exprMn wn1 mul1r rootCK. by rewrite ReMr ?ltr0_real // ltW // nmulr_lgt0. without loss leI0z: z zn_x leR0z / 'Im z >= 0. move=> IHz; have: 'Im z \is real by []. case/real_ge0P=> [|/ltW leIz0]; first exact: IHz. apply: (IHz z^* ); rewrite ?Re_conj ?Im_conj ?oppr_ge0 //. by rewrite -rmorphXn /= zn_x conj_Creal. by apply: le_trans leR0z _; rewrite -Re_y ?rootC_Re_max ?ltr0_real. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)