no goals
α : Type ?u.185497
x y z : ℝ
l : Filter α
n : ℕ
⊢ (fun x => x ^ n) =o[atTop] exp
simpa [isLittleO_iff_tendsto fun x hx => ((exp_pos x).ne' hx).elim] using
  tendsto_div_pow_mul_exp_add_atTop 1 0 n zero_ne_one