Skip to content

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

Robbert Krebbers requested to merge robbert/take_drop_reverse into master

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.

Edited by Robbert Krebbers

Merge request reports