no goals
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
⊢ (fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]
simp only [div_eq_mul_inv, preimage_mul_const_uIcc (inv_ne_zero ha), inv_inv]