English
The sum of two angles with swapped middle point equals the angle with non-swapped order: ∡ p2 p p3 + ∡ p1 p p2 = ∡ p1 p p3.
Русский
Сумма углов с перестановкой средней точки равна углу без перестановки: ∡ p2 p p3 + ∡ p1 p p2 = ∡ p1 p p3.
LaTeX
$$$ \forall p,p_1,p_2,p_3 : P,\ (p_1 \neq p) \land (p_2 \neq p) \land (p_3 \neq p) \rightarrow\ (\angle p_2 p p_3 + \angle p_1 p p_2) = \angle p_1 p p_3$$$
Lean4
/-- Given three points not equal to `p`, the angle between the first and the second at `p` plus
the angle between the second and the third equals the angle between the first and the third. -/
@[simp]
theorem oangle_add {p p₁ p₂ p₃ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) (hp₃ : p₃ ≠ p) : ∡ p₁ p p₂ + ∡ p₂ p p₃ = ∡ p₁ p p₃ :=
o.oangle_add (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂) (vsub_ne_zero.2 hp₃)
