[STATEMENT]
lemma eventually_nonzero_ln_const'_at_top [eventually_nonzero_simps]:
  "b > 0 \<Longrightarrow> eventually_nonzero at_top (\<lambda>x. ln (x * b :: real))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < b \<Longrightarrow> eventually_nonzero at_top (\<lambda>x. ln (x * b))
[PROOF STEP]
using eventually_nonzero_ln_const_at_top[of b]
[PROOF STATE]
proof (prove)
using this:
0 < b \<Longrightarrow> eventually_nonzero at_top (\<lambda>x. ln (b * x))

goal (1 subgoal):
 1. 0 < b \<Longrightarrow> eventually_nonzero at_top (\<lambda>x. ln (x * b))
[PROOF STEP]
by (simp add: mult.commute)