proposition: Lemma rootnE n x y : 0 < n -> y ^ n <= x < y.+1 ^ n -> rootn n x = y.
proof: Proof. move=> n_gt0 /andP[ynLx xLySn]. have /andP[rLx xLrS] := rootn_bound x n_gt0. apply/eqP; rewrite eqn_leq. rewrite -ltnS -(ltn_exp2r _ _ n_gt0) (leq_ltn_trans rLx) //. by rewrite -ltnS -(ltn_exp2r _ _ n_gt0) (leq_ltn_trans ynLx). Qed.
imports: mathcomp(all_ssreflect)