English
For three points P1, P2, P3 with P1+P2+P3 = O, a cyclic relation holds among their y-coordinates and x-coordinates: y1(x2 - x3) + y2(x3 - x1) + y3(x1 - x2) = 0.
Русский
Для трёх точек P1, P2, P3 с P1+P2+P3 = O выполняется циклическое тождество между их y-координатами и x-координатами.
LaTeX
$$$ y_1 (x_2 - x_3) + y_2 (x_3 - x_1) + y_3 (x_1 - x_2) = 0, \quad x_3 = W.addX\, x_1 x_2 (W.slope x_1 x_2 y_1 y_2), \quad y_3 = W.addY x_1 x_2 y_1 (W.slope x_1 x_2 y_1 y_2) $$$
Lean4
/-- The formula `y(P₁)(x(P₂) - x(P₃)) + y(P₂)(x(P₃) - x(P₁)) + y(P₃)(x(P₁) - x(P₂)) = 0`,
assuming that `P₁ + P₂ + P₃ = O`. -/
theorem cyclic_sum_Y_mul_X_sub_X {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) :
let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)
y₁ * (x₂ - x₃) + y₂ * (x₃ - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0 :=
by
simp_rw [slope_of_X_ne hx, negAddY, addX]
simp [field, sub_ne_zero.mpr hx]
ring1
