This MR contains two commits: One with the actual lemmas, and one to perform some rearrangements. To prove the
_r variant, I needed properties of
reverse. I thus moved the
reverse lemmas above the
The lemmas in this MR generalize the ones in !356 (merged). They also allow proving a variant for
suffix_of, which is missing in that MR.