∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Nonsingular Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          ¬(P 0 * Q 2 = Q 0 * P 2 ∧ P 1 * Q 2 = W.negY Q * P 2) →
            WeierstrassCurve.Projective.Point.toAffine W
                ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  1] =
              WeierstrassCurve.Projective.Point.toAffine W P + WeierstrassCurve.Projective.Point.toAffine W Q