no goals
α : Type ?u.97427
β : Type ?u.97430
ι : Type ?u.97433
R : Type u_1
inst✝ : NormedRing R
r : ℝ
hr : 1 < r
⊢ Nat.cast =o[atTop] fun n => r ^ n
simpa only [pow_one] using @isLittleO_pow_const_const_pow_of_one_lt R _ 1 _ hr