Add lemmas for `reverse` of `take`/`drop`.

The first two lemmas are in the stdlib for rev (the quadratic reverse), I use those proofs to establish a version for std++'s reverse (the linear version).

I also add two useful corollaries.