feat(geometry/euclidean/basic): `dist_center_eq_dist_center_of_mem_sphere'` (#17390)
feat(geometry/euclidean/basic): `dist_center_eq_dist_center_of_mem_sphere'` (#17390)

Add a variant of `dist_center_eq_dist_center_of_mem_sphere`, but with the distances the other way round (analogous to the pair of lemmas `mem_sphere` and `mem_sphere'`).







leanprover-community/mathlib,leanprover-community/mathlib