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.
