proposition: Lemma rootC_leq (m n : nat) x : 1 <= x -> (0 < n)%N -> (n <= m)%N -> m.-root x <= n.-root x.
proof: Proof. move=> Hx Hn Hmn. have x_ge0 : 0 <= x by apply: le_trans Hx. rewrite root_le_x -?rootCX ?root_x_le ?exprn_ge0 //; first exact: exp_incr_expp. by rewrite expr0n; case: eqP. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)