Formalizing some basic hyperbolic geometry

This is in the very early stages and experimental and has lots of sorry's...