proposition: Lemma rootCMl n x z : 0 <= x -> n.-root (x * z) = n.-root x * n.-root z.
proof: Proof. rewrite le0r => /predU1P[-> | x_gt0]; first by rewrite !(mul0r, rootC0). have [| n_gt1 | ->] := ltngtP n 1; last by rewrite !root1C. by case: n => //; rewrite !root0C mul0r. have [x_ge0 n_gt0] := (ltW x_gt0, ltnW n_gt1). have nx_gt0: 0 < n.-root x by rewrite rootC_gt0. have Rnx: n.-root x \is real by rewrite ger0_real ?ltW. apply: eqC_semipolar; last 1 first; try apply/eqP. - by rewrite ImMl // !(Im_rootC_ge0, mulr_ge0, rootC_ge0). - by rewrite -(eqrXn2 n_gt0) // -!normrX exprMn !rootCK. rewrite eq_le; apply/andP; split; last first. rewrite rootC_Re_max ?exprMn ?rootCK ?ImMl //. by rewrite mulr_ge0 ?Im_rootC_ge0 ?ltW. rewrite -[n.-root _](mulVKf (negbT (gt_eqF nx_gt0))) !(ReMl Rnx) //. rewrite ler_pM2l // rootC_Re_max ?exprMn ?exprVn ?rootCK ?mulKf ?gt_eqF //. by rewrite ImMl ?rpredV // mulr_ge0 ?invr_ge0 ?Im_rootC_ge0 ?ltW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)