set n := ⌊b⌋ - ⌊a⌋ with hn
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
⊢ 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 : ℤ := ⌊b⌋ - ⌊a⌋
hn : n = ⌊b⌋ - ⌊a⌋
⊢ P a b