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