Random collection of lemmas from RefinedC

These are some things from RefinedC that I would like to upstream to stdpp. There are still some open questions, see the comments for them. Please let me know which of these changes make sense in stdpp.