α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p (reverse l) <:+ reverse l
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rdropWhile p l <+: l
rw [← reverse_suffix, rdropWhile, reverse_reverse]
no goals
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ dropWhile p (reverse l) <:+ reverse l
exact dropWhile_suffix _