have : 0 ≤ n := by simp only [hn, sub_nonneg, ge_iff_le, Int.floor_le_floor _ _ (hab.le)]
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
a b : ℝ
hab : a < b
n : ℤ
hn : n = ⌊b⌋ - ⌊a⌋
this : 0 ≤ n
⊢ P a b