English
If the doubled-oriented angles satisfy the two-angle equality, the four points are either concyclic or collinear (in a suitable sense).
Русский
Если двойные ориентированные углы удовлетворяют равенству двухуглов, четыре точки либо конциклически лежат на одной окружности, либо коллинеарны.
LaTeX
$$$\text{Concyclic or Collinear}\{p_1,p_2,p_3,p_4\}$ given $2\angle(p_1,p_2,p_4)=2\angle(p_1,p_3,p_4)$.$$
Lean4
/-- Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral
add to π", for oriented angles mod π, with a "concyclic or collinear" conclusion. -/
theorem concyclic_or_collinear_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ : P}
(h : (2 : ℤ) • ∡ p₁ p₂ p₄ = (2 : ℤ) • ∡ p₁ p₃ p₄) :
Concyclic ({ p₁, p₂, p₃, p₄ } : Set P) ∨ Collinear ℝ ({ p₁, p₂, p₃, p₄ } : Set P) :=
by
rcases cospherical_or_collinear_of_two_zsmul_oangle_eq h with (hc | hc)
· exact Or.inl ⟨hc, coplanar_of_fact_finrank_eq_two _⟩
· exact Or.inr hc
