mathlib

2b80d2f6 - feat(geometry/euclidean/sphere): proof of Freek thm 95 - Ptolemy’s Theorem (#7329)

feat(geometry/euclidean/sphere): proof of Freek thm 95 - Ptolemy’s Theorem (#7329) Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>