∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂ (Polynomial.C y₂) =
          WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂
            (WeierstrassCurve.Affine.linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))