This upstreams some lemmas from Perennial (so I assume the proofs are by @tchajed; I ported them to the non-ssreflect world of std++).