[STATEMENT]
lemma smallo_real_nat_transfer:
  "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> o(g) \<Longrightarrow> (\<lambda>x. f (real x)) \<in> o(\<lambda>x. g (real x))
[PROOF STEP]
by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])