right_ne_of_oangle_eq_neg_pi_div_two

English

If the right angle is nonzero, then the last two points are not equal.

Русский

Если правый угол ненулевой, последние две точки не равны.

LaTeX

$$$\\angle p_1 p_2 p_3 \\neq 0 \\Rightarrow p_3 \\neq p_2$$$

Lean4

/-- If the angle between three points is `-π / 2`, the last two points are not equal. -/
theorem right_ne_of_oangle_eq_neg_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = (-π / 2 : ℝ)) : p₃ ≠ p₂ :=
  right_ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

Похожие утверждения