case refl
m✝ n✝ k✝ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k : ℕ
mn : m ≤ n
hP✝ : P k
hP : P n
⊢ decreasingInduction h (_ : m ≤ n) hP = decreasingInduction h mn (decreasingInduction h (_ : Nat.le n n) hP)

case step
m✝ n✝ k✝¹ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k✝ : ℕ
mn : m ≤ n
hP✝ : P k✝
k : ℕ
nk : Nat.le n k
ih : ∀ (hP : P k), decreasingInduction h (_ : m ≤ k) hP = decreasingInduction h mn (decreasingInduction h nk hP)
hP : P (succ k)
⊢ decreasingInduction h (_ : m ≤ succ k) hP =
    decreasingInduction h mn (decreasingInduction h (_ : Nat.le n (succ k)) hP)
m✝ n✝ k✝ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k : ℕ
mn : m ≤ n
nk : n ≤ k
hP : P k
⊢ decreasingInduction h (_ : m ≤ k) hP = decreasingInduction h mn (decreasingInduction h nk hP)
induction' nk with k nk ih
no goals
case refl
m✝ n✝ k✝ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k : ℕ
mn : m ≤ n
hP✝ : P k
hP : P n
⊢ decreasingInduction h (_ : m ≤ n) hP = decreasingInduction h mn (decreasingInduction h (_ : Nat.le n n) hP)
rw [decreasingInduction_self]
no goals
case step
m✝ n✝ k✝¹ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k✝ : ℕ
mn : m ≤ n
hP✝ : P k✝
k : ℕ
nk : Nat.le n k
ih : ∀ (hP : P k), decreasingInduction h (_ : m ≤ k) hP = decreasingInduction h mn (decreasingInduction h nk hP)
hP : P (succ k)
⊢ decreasingInduction h (_ : m ≤ succ k) hP =
    decreasingInduction h mn (decreasingInduction h (_ : Nat.le n (succ k)) hP)
rw [decreasingInduction_succ h (le_trans mn nk), ih, decreasingInduction_succ]