no goals
α : Type u
β : Type v
γ : Type w
as : List α
i : Nat
h : length as ≤ i
⊢ drop i as = nil
match as, i with
| [],    i   => simp
| _::_,  0   => simp at h
| _::as, i+1 => simp at h; exact @drop_eq_nil_of_le as i (Nat.le_of_succ_le_succ h)
no goals
α : Type u
β : Type v
γ : Type w
as : List α
i✝ i : Nat
h : length nil ≤ i
⊢ drop i nil = nil
simp
no goals
α : Type u
β : Type v
γ : Type w
as : List α
i : Nat
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝) ≤ 0
⊢ drop 0 (head✝ :: tail✝) = nil
simp at h
α : Type u
β : Type v
γ : Type w
as✝ : List α
i✝ : Nat
head✝ : α
as : List α
i : Nat
h : Nat.succ (length as) ≤ i + 1
⊢ drop (i + 1) (head✝ :: as) = nil
α : Type u
β : Type v
γ : Type w
as✝ : List α
i✝ : Nat
head✝ : α
as : List α
i : Nat
h : length (head✝ :: as) ≤ i + 1
⊢ drop (i + 1) (head✝ :: as) = nil
simp at h
no goals
α : Type u
β : Type v
γ : Type w
as✝ : List α
i✝ : Nat
head✝ : α
as : List α
i : Nat
h : Nat.succ (length as) ≤ i + 1
⊢ drop (i + 1) (head✝ :: as) = nil
exact @drop_eq_nil_of_le as i (Nat.le_of_succ_le_succ h)