[STATEMENT]
lemma one_smallo_powr: "e > (0::real) \<Longrightarrow> (\<lambda>_. 1) \<in> o(\<lambda>x. x powr e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < e \<Longrightarrow> (\<lambda>_. 1) \<in> o(\<lambda>x. x powr e)
[PROOF STEP]
by (auto simp: smallomega_iff_smallo [symmetric] real_powr_at_top 
                 smallomegaI_filterlim_at_top_norm)