no goals
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑↑(↑translate (↑Multiplicative.ofAdd x))^[n + 1]) 0 / (↑n + 1)) atTop (𝓝 x)
simp only [translate_iterate, translate_apply, add_zero, Nat.cast_succ,
  mul_div_cancel_left (G₀ := ℝ) _ (Nat.cast_add_one_ne_zero _), tendsto_const_nhds]