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

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

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