[Merged by Bors] - feat(Geometry/Euclidean/Sphere): add lemmas about points on a sphere#41143

Scarlett-le wants to merge 2 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

Scarlett-le:sphere-ne-centerScarlett-le/mathlib4:sphere-ne-centerCopy head branch name to clipboard