proposition: Lemma rootC_Re_max n x y : (n > 0)%N -> y ^+ n = x -> 0 <= 'Im y -> 'Re y <= 'Re (n.-root x).
proof: Proof. by move=> n_gt0 yn_x leI0y; case_rootC=> z /= _ /(_ y n_gt0 yn_x)/argCleP[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)