EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical

theorem EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {a b c d p : P}, EuclideanGeometry.Cospherical {a, b, c, d} → EuclideanGeometry.angle a p c = Real.pi → EuclideanGeometry.angle b p d = Real.pi → dist a b * dist c d + dist b c * dist d a = dist a c * dist b d

**Ptolemy’s Theorem**: In Euclidean geometry, given a set of four points `{a, b, c, d}` that are cospherical (i.e., all the points are equidistant from some point `p`), if the angle at `p` between `a` and `c` is π (180 degrees), and similarly, the angle between `b` and `d` is also π, then the product of the distances between `a` and `b` and between `c` and `d`, plus the product of the distances between `b` and `c` and between `d` and `a`, is equal to the product of the distances between `a` and `c` and between `b` and `d`. In mathematical notation, this can be expressed as `dist(a, b) * dist(c, d) + dist(b, c) * dist(d, a) = dist(a, c) * dist(b, d)`.

More concisely: In Euclidean geometry, if four cospherical points {a, b, c, d} satisfy the condition that the angles at the center of the sphere between a and c, and between b and d are each π (180 degrees), then the product of the inter-point distances (a, b) and (c, d), plus the product of the inter-point distances (b, c) and (d, a), equals the product of the inter-point distances (a, c) and (b, d).