case refl
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ P m (_ : Nat.le m m)

case step
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ ∀ {m_1 : ℕ} (a : Nat.le m m_1), P m_1 a → P (Nat.succ m_1) (_ : Nat.le m (Nat.succ m_1))
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ ∀ (n : ℕ) (hn : m ≤ n), P n hn
apply Nat.le.rec
no goals
case refl
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ P m (_ : Nat.le m m)
exact base
case step
m✝ n✝ k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
n : ℕ
hn : Nat.le m n
⊢ P n hn → P (Nat.succ n) (_ : Nat.le m (Nat.succ n))
case step
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ ∀ {m_1 : ℕ} (a : Nat.le m m_1), P m_1 a → P (Nat.succ m_1) (_ : Nat.le m (Nat.succ m_1))
intros n hn
no goals
case step
m✝ n✝ k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
n : ℕ
hn : Nat.le m n
⊢ P n hn → P (Nat.succ n) (_ : Nat.le m (Nat.succ n))
apply succ n hn