feat(geometry/euclidean/basic): `concyclic` (#16927)
Define a set of points to be concyclic if it is cospherical and coplanar. I don't expect that much use of this definition, as opposed to the separate `cospherical` and `coplanar` pieces, in mathlib, but it's intended to allow formal statements of results involving concyclic points that correspond more closely to the informal statements.
