proposition: Lemma Im_rootC_ge0 n x : (n > 1)%N -> 0 <= 'Im (n.-root x).
proof: Proof. set y := n.-root x => n_gt1; have n_gt0 := ltnW n_gt1. apply: wlog_neg; rewrite -real_ltNge ?rpred0 // => ltIy0. suffices [z zn_x leI0z]: exists2 z, z ^+ n = x & 'Im z >= 0. by rewrite /y; case_rootC => /= y1 _ /(_ z n_gt0 zn_x)/argCleP[]. have [w wn1 ltRw0] := neg_unity_root n_gt1. wlog leRI0yw: w wn1 ltRw0 / 0 <= 'Re y * 'Im w. move=> IHw; have: 'Re y * 'Im w \is real by rewrite rpredM. case/real_ge0P=> [|/ltW leRIyw0]; first exact: IHw. apply: (IHw w^* ); rewrite ?Re_conj ?Im_conj ?mulrN ?oppr_ge0 //. by rewrite -rmorphXn wn1 rmorph1. exists (w * y); first by rewrite exprMn wn1 mul1r rootCK. rewrite [w]Crect [y]Crect mulC_rect. by rewrite Im_rect ?rpredD ?rpredN 1?rpredM // addr_ge0 // ltW ?nmulr_rgt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)