# Ptolemy's theorem #

This file proves Ptolemy's theorem on the lengths of the diagonals and sides of a cyclic quadrilateral.

## Main theorems #

`mul_dist_add_mul_dist_eq_mul_dist_of_cospherical`

: Ptolemy’s Theorem (Freek No. 95).

TODO: The current statement of Ptolemy’s theorem works around the lack of a "cyclic polygon" concept in mathlib, which is what the theorem statement would naturally use (or two such concepts, since both a strict version, where all vertices must be distinct, and a weak version, where consecutive vertices may be equal, would be useful; Ptolemy's theorem should then use the weak one).

An API needs to be built around that concept, which would include:

- strict cyclic implies weak cyclic,
- weak cyclic and consecutive points distinct implies strict cyclic,
- weak/strict cyclic implies weak/strict cyclic for any subsequence,
- any three points on a sphere are weakly or strictly cyclic according to whether they are distinct,
- any number of points on a sphere intersected with a two-dimensional affine subspace are cyclic in some order,
- a list of points is cyclic if and only if its reversal is,
- a list of points is cyclic if and only if any cyclic permutation is, while other permutations are not when the points are distinct,
- a point P where the diagonals of a cyclic polygon cross exists (and is unique) with weak/strict betweenness depending on weak/strict cyclicity,
- four points on a sphere with such a point P are cyclic in the appropriate order, and so on.

theorem
EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical
{V : Type u_1}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
{P : Type u_2}
[MetricSpace P]
[NormedAddTorsor V P]
{a : P}
{b : P}
{c : P}
{d : P}
{p : P}
(h : EuclideanGeometry.Cospherical {a, b, c, d})
(hapc : EuclideanGeometry.angle a p c = Real.pi)
(hbpd : EuclideanGeometry.angle b p d = Real.pi)
:

**Ptolemy’s Theorem**.