∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  p ∈ s → (s.IsTangentAt p (affineSpan ℝ {p, q}) ↔ EuclideanGeometry.angle q p s.center = Real.pi / 2)