Commit 2023-03-16 11:15 eea141bc

refactor(geometry/euclidean): split out spheres (#18220) Rearrange material related to spheres as follows:

• geometry.euclidean.sphere.power has most of the content from the previous geometry.euclidean.sphere (intersecting chords / secants, which at some point should probably be refactored using an explicit definition of the power of a point).
• geometry.euclidean.sphere.ptolemy has the proof of Ptolemy's theorem that was previously in geometry.euclidean.sphere.
• geometry.euclidean.sphere.basic has most of the material previously in geometry.euclidean.basic: definitions of sphere, cospherical and concyclic and associated lemmas.
• geometry.euclidean.sphere.second_inter has the definition and lemmas about second_inter. There are no changes to API or proofs.