English
Replacing the first and third points by points on opposite rays leaves the oriented angle signs equal.
Русский
Замена первой и третьей точек точками на противоположных лучах сохраняет знаки угла.
LaTeX
$$$(\angle p_1 p_2 p_3).sign = (\angle p_1' p_2 p_3').sign$$$
Lean4
/-- Given three points in strict order on the same line, and a fourth point, the angles at the
fourth point between the first and second or second and third points have the same sign. -/
theorem _root_.Sbtw.oangle_sign_eq {p₁ p₂ p₃ : P} (p₄ : P) (h : Sbtw ℝ p₁ p₂ p₃) :
(∡ p₁ p₄ p₂).sign = (∡ p₂ p₄ p₃).sign :=
haveI hc : Collinear ℝ ({ p₁, p₂, p₂, p₃ } : Set P) := by simpa using h.wbtw.collinear
hc.oangle_sign_of_sameRay_vsub _ h.left_ne h.ne_right h.wbtw.sameRay_vsub
