English
Swapping the first and second points in an oriented angle negates its sign: -(∡ p1 p2 p3).sign = (∡ p2 p1 p3).sign.
Русский
Поменяв местами первые две точки, знак ориентированного угла меняется на противоположный: -(∡ p1 p2 p3).sign = (∡ p2 p1 p3).sign.
LaTeX
$$$- (\measuredangle p_1 p_2 p_3).sign = (\measuredangle p_2 p_1 p_3).sign$$$
Lean4
/-- Swapping the first and second points in an oriented angle negates the sign of that angle. -/
theorem oangle_swap₁₂_sign (p₁ p₂ p₃ : P) : -(∡ p₁ p₂ p₃).sign = (∡ p₂ p₁ p₃).sign :=
by
rw [eq_comm, oangle, oangle, ← o.oangle_neg_neg, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, ←
vsub_sub_vsub_cancel_left p₁ p₃ p₂, ← neg_vsub_eq_vsub_rev p₃ p₂, sub_eq_add_neg, neg_vsub_eq_vsub_rev p₂ p₁,
add_comm, ← @neg_one_smul ℝ]
nth_rw 2 [← one_smul ℝ (p₁ -ᵥ p₂)]
rw [o.oangle_sign_smul_add_smul_right]
simp
