rw [Finset.mem_Icc, mem_Icc, ceil_mul_le_iff hx, le_floor_mul_iff hb hx]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hb : 0 ≤ b
hx : 0 < x
⊢ n ∈ Finset.Icc ⌈a * x⌉₊ ⌊b * x⌋₊ ↔ ↑n / x ∈ Icc a b
no goals