[STATEMENT]
lemma ani_omega:
  "ani(x)\<^sup>\<omega> = ani(x) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani x\<^sup>\<omega> = ani x * L
[PROOF STEP]
by (simp add: L_left_zero ani_def mult_L_omega mult_assoc)