proposition: Lemma leq_rootn n x y : 0 < n -> x <= y -> rootn n x <= rootn n y.
proof: Proof. move=> n_gt0 xLy. rewrite -ltnS -(ltn_exp2r _ _ n_gt0). have /andP[rLx _] := rootn_bound x n_gt0. have /andP[_ yLr] := rootn_bound y n_gt0. by apply: leq_ltn_trans rLx (leq_ltn_trans _ yLr). Qed.
imports: mathcomp(all_ssreflect)