exact_mod_cast (by linarith)
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (P : ℝ → ℝ → Prop),
      (∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b) →
        (∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c) →
          ∀ (a b : ℝ), a < b → ↑m = ⌊b⌋ - ⌊a⌋ → P a b
P : ℝ → ℝ → Prop
base : ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
step : ∀ (a : ℝ) (k : ℤ) (c : ℝ), a < ↑k → ↑k < c → P a ↑k → P (↑k) c → P a c
a b : ℝ
x✝ : a < b
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
hn : ↑n + 1 = ⌊b⌋ - ⌊a⌋
⊢ ↑⌊a⌋ + 1 ≤ ↑⌊b⌋
no goals