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