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 elem_of lemmas.
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.
/cc @jihgfee