The lemmas in this directory should be added to the stdlib and removed from corn. https://github.com/coq-community/corn/tree/master/stdlib_omissions