[STATEMENT]
lemma ani_mult_left_upper_bound:
  "ani(x * y) \<le> ani(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani (x * y) \<le> ani x
[PROOF STEP]
by (simp add: an_mult_left_upper_bound ani_def mult_left_isotone)