∀ {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₂) →
        W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
          -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) *
              (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))