proposition: Lemma rootn_ltn n x y : 0 < n -> x < y.+1 ^ n -> rootn n x <= y.
proof: Proof. move=> n_gt0; rewrite ltnNge [in X in _ -> X]leqNgt. apply: contra => yLrx. have /andP[rLx _] := rootn_bound x n_gt0. by apply: leq_trans rLx; rewrite leq_exp2r. Qed.
imports: mathcomp(all_ssreflect)