Physlib.Mathematics.ForMathlib.List

Let $I$ be a type and $P$ be a decidable predicate on $I$. Let $l$ be a list of elements of type $I$. Suppose that for any indices $i, j$ such that $0 \le i < j < \text{length}(l)$, if the element at index $j$ satisfies $P$, then the element at index $i$ must also satisfy $P$ (i.e., the property $P$ is "prefix-closed" on $l$). Then, for any index $k$, removing the $k$-th element from $l$ and then taking the longest prefix of elements satisfying $P$ is equivalent to taking the longest prefix of $l$ satisfying $P$ and then removing its $k$-th element.