List.rdropWhile_concat

theorem List.rdropWhile_concat : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (x : α), List.rdropWhile p (l ++ [x]) = if p x = true then List.rdropWhile p l else l ++ [x]

The theorem `List.rdropWhile_concat` states that, for any type `α`, a predicate function `p` from `α` to `Bool`, a list `l` of elements of type `α`, and an element `x` of type `α`, the function `List.rdropWhile` applied to the list obtained by concatenating `l` and a singleton list containing `x` is equal to: if the predicate `p` applied to `x` is `true`, then `List.rdropWhile p l`, otherwise the list obtained by concatenating `l` and the singleton list containing `x`. In essence, it says that if the last element of the list satisfies the predicate, it will be dropped, otherwise the list remains the same after applying `List.rdropWhile`.

More concisely: For any type `α`, list `l` of length `n+1` in `α`, predicate `p : α → Bool`, and `x ∈ α`, if `p(x)` then `List.rdropWhile p (l ++ [x]) = List.rdropWhile p l`, otherwise `List.rdropWhile p (l ++ [x]) = l ++ [x]`.