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

State before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ k ≤ length (head :: tail) → pred k ≤ length tail
Tactic:
rw [length, <-nat_succ_eq_plus_one]
State after:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ k ≤ succ (length tail) → pred k ≤ length tail

State before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ k ≤ succ (length tail) → pred k ≤ length tail
Tactic:
apply nat_pred_le_succ
State after:
no goals