These are some lemmas which I need in my development. @robbertkrebbers and I talked about some of them today. I will make another MR with the rotate function. Let me know what you think and which lemmas seem useful. Also better proofs are always appreciated.