apply le_trans (Int.floor_le x) <| le_trans (hx.1 ▸ this) (by simp)
case inl
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ ↑⌊x⌋ ≤ max |a| |b| + 1
no goals