no goals
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : 0 ≤ a
hbc : b ≤ c
⊢ (fun x x_1 => x * x_1) a '' Icc b c = Icc (a * b) (a * c)
convert image_mul_right_Icc hbc ha using 1 <;> simp only [mul_comm _ a]