Theorem: list_length_cons_le_succ (Katydid/Std/Lists.lean)

State before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ length (head :: tail) ≤ succ k → length tail ≤ k
Tactic:
rw [length]
State after:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ length tail + 1 ≤ succ k → length tail ≤ k

State before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ length tail + 1 ≤ succ k → length tail ≤ k
Tactic:
apply Nat.le_of_succ_le_succ
State after:
no goals