re-implement lemmas to avoid copyright issues, change name of the file containing those lemmas

some lemmas had been ported from HoTT library, and as I am not sure how that counts as copying in the sense of copyright, I reimplemented them.