α : Type u_1
β : Type ?u.876
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
n : ℕ
h : Pairwise R (a :: l)
⊢ Pairwise R (List.drop n l)
α : Type u_1
β : Type ?u.876
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
n : ℕ
h : Pairwise R (a :: l)
⊢ Pairwise R (List.drop (n + 1) (a :: l))
rw [List.drop]
no goals
α : Type u_1
β : Type ?u.876
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
n : ℕ
h : Pairwise R (a :: l)
⊢ Pairwise R (List.drop n l)
exact Pairwise.drop (pairwise_cons.mp h).right