by_cases b_le_flaP1 : b = ⌊a⌋ + 1
case hi
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
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
⊢ P a b
case pos
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
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : b = ↑⌊a⌋ + 1
⊢ P a b

case neg
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
hn : ↑n.succ = ⌊b⌋ - ⌊a⌋
Pa : P a (↑⌊a⌋ + 1)
b_le_flaP1 : ¬b = ↑⌊a⌋ + 1
⊢ P a b