m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
mn : m ≤ n
msn : m ≤ n + 1
hP : P (n + 1)
⊢ leRecOn msn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) hP =
    leRecOn mn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) (h n hP)
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
mn : m ≤ n
msn : m ≤ n + 1
hP : P (n + 1)
⊢ decreasingInduction h msn hP = decreasingInduction h mn (h n hP)
dsimp only [decreasingInduction]
no goals
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
mn : m ≤ n
msn : m ≤ n + 1
hP : P (n + 1)
⊢ leRecOn msn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) hP =
    leRecOn mn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) (h n hP)
rw [leRecOn_succ]