English
For points on a circle, the angle at the center equals π minus twice the angle at the base vertex pair.
Русский
Угол в центре равен π минус дважды угол у основания для точек на окружности.
LaTeX
$$$\\angle p_1 s.center p_2 = \\pi - 2\\,\\angle p_2 p_1 s.center$$$
Lean4
/-- Oriented angle version of "angles in same segment are equal" and "opposite angles of a
cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result),
represented here as equality of twice the angles. -/
theorem two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ : P} (h : Cospherical ({ p₁, p₂, p₃, p₄ } : Set P)) (hp₂p₁ : p₂ ≠ p₁)
(hp₂p₄ : p₂ ≠ p₄) (hp₃p₁ : p₃ ≠ p₁) (hp₃p₄ : p₃ ≠ p₄) : (2 : ℤ) • ∡ p₁ p₂ p₄ = (2 : ℤ) • ∡ p₁ p₃ p₄ :=
by
obtain ⟨s, hs⟩ := cospherical_iff_exists_sphere.1 h
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff, Sphere.mem_coe] at hs
exact Sphere.two_zsmul_oangle_eq hs.1 hs.2.1 hs.2.2.1 hs.2.2.2 hp₂p₁ hp₂p₄ hp₃p₁ hp₃p₄
