Add some lemmas

I'm new at contributing to this repository, so please let me know if I violated any conventions.  One thing I wasn't sure about was that in promoting the 'aux' lemmas from Univalence into public named ones, I thought they would go better in PathOver, but putting them there required reordering the imports.