α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ takeWhile p (reverse l) <+: reverse l
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ rtakeWhile p l <:+ l
rw [← reverse_prefix, rtakeWhile, reverse_reverse]
no goals
α : Type u_1
p : α → Bool
l : List α
n : ℕ
⊢ takeWhile p (reverse l) <+: reverse l
exact takeWhile_prefix _