α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ ∀ (hl : 0 < length (dropWhile p l)), ¬p (nthLe (dropWhile p l) 0 hl) = true
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p (dropWhile p l) = dropWhile p l
simp only [dropWhile_eq_self_iff]
no goals
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ ∀ (hl : 0 < length (dropWhile p l)), ¬p (nthLe (dropWhile p l) 0 hl) = true
exact fun h => dropWhile_nthLe_zero_not p l h