proposition: Lemma norm_rootC n x : `|n.-root x| = n.-root `|x|.
proof: Proof. have [-> | n_gt0] := posnP n; first by rewrite !root0C normr0. by apply/eqP; rewrite -(eqrXn2 n_gt0) ?rootC_ge0 // -normrX !rootCK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)