English
If x1 ≠ x2, then the x-coordinate of P1+P2 along the line with slope is given by a rational expression in x1, x2, y1, y2.
Русский
Если x1 ≠ x2, то x-координата суммы P1+P2 по прямой с наклоном задаётся рациональным выражением через x1, x2, y1, y2.
LaTeX
$$$ x_3 = W.addX x_1 x_2 (W.slope x_1 x_2 y_1 y_2) = W.addX x_1 x_2 (W.slope x_1 x_2 y_1 (W.negY x_2 y_2)) - \frac{(y_1 - W.negY x_1 y_1) (y_2 - W.negY x_2 y_2)}{(x_2 - x_1)^2} $$$
Lean4
/-- The formula `ψ(P₁ + P₂) = (ψ(P₂)(x(P₁) - x(P₃)) - ψ(P₁)(x(P₂) - x(P₃))) / (x(P₂) - x(P₁))`,
where `ψ(x,y) = 2y + a₁x + a₃`. -/
theorem addY_sub_negY_addY {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) :
let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)
let y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)
y₃ - W.negY x₃ y₃ = ((y₂ - W.negY x₂ y₂) * (x₁ - x₃) - (y₁ - W.negY x₁ y₁) * (x₂ - x₃)) / (x₂ - x₁) :=
by
simp_rw [addY, negY, eq_div_iff (sub_ne_zero.mpr hx.symm)]
linear_combination (norm := ring1) 2 * cyclic_sum_Y_mul_X_sub_X y₁ y₂ hx
