mathlib3

afa6b72e - feat(geometry/euclidean): proof of Freek thm 55 - product of chords (#7139)

feat(geometry/euclidean): proof of Freek thm 55 - product of chords (#7139) proof of thm 55 Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>