ι : Type ?u.46927
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hn : n ≠ 0
h : length l ≤ n - 1
⊢ length (a :: l) ≤ n
ι : Type ?u.46927
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hn : n ≠ 0
h : n < length (a :: l)
⊢ n - 1 < length l
contrapose! h
ι : Type ?u.46927
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hn : n ≠ 0
h : length l ≤ n - 1
⊢ succ (length l) ≤ n
ι : Type ?u.46927
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hn : n ≠ 0
h : length l ≤ n - 1
⊢ length (a :: l) ≤ n
rw [length_cons]
case h.e'_4
ι : Type ?u.46927
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hn : n ≠ 0
h : length l ≤ n - 1
⊢ n = succ (n - 1)
ι : Type ?u.46927
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hn : n ≠ 0
h : length l ≤ n - 1
⊢ succ (length l) ≤ n
convert succ_le_succ h
no goals
case h.e'_4
ι : Type ?u.46927
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
n : ℕ
hn : n ≠ 0
h : length l ≤ n - 1
⊢ n = succ (n - 1)
exact (Nat.succ_pred_eq_of_pos hn.bot_lt).symm