case zero
n k l : ℕ
⊢ zero ≤ succ n → pred zero ≤ n

case succ
n k l n✝ : ℕ
⊢ succ n✝ ≤ succ n → pred (succ n✝) ≤ n
m n k l : ℕ
⊢ m ≤ succ n → pred m ≤ n
cases m
no goals
case succ
n k l n✝ : ℕ
⊢ succ n✝ ≤ succ n → pred (succ n✝) ≤ n
exact le_of_succ_le_succ
no goals
case zero
n k l : ℕ
⊢ zero ≤ succ n → pred zero ≤ n
exact fun _ => zero_le n