English
If p2 p1 p1' are in weak betweenness and p1' ≠ p2, the angle signs are preserved: (∡ p1 p2 p3).sign = (∡ p1' p2 p3).sign.
Русский
Если p2 между p1 и p1', знак угла сохраняется: ∡ p1 p2 p3 и ∡ p1' p2 p3 имеют одинаковый знак.
LaTeX
$$$Wbtw_\mathbb{R}(p_2,p_1,p_1') \Rightarrow (\angle p_1 p_2 p_3).sign = (\angle p_1' p_2 p_3).sign$$$
Lean4
/-- Given three points in weak order on the same line, with the second not equal to the third,
and a fourth point, the angles at the fourth point between the second and third or first and
third points have the same sign. -/
theorem _root_.Wbtw.oangle_sign_eq_of_ne_right {p₁ p₂ p₃ : P} (p₄ : P) (h : Wbtw ℝ p₁ p₂ p₃) (hne : p₂ ≠ p₃) :
(∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign := by
simp_rw [oangle_rev p₃, Real.Angle.sign_neg, h.symm.oangle_sign_eq_of_ne_left _ hne.symm]
