∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      ∀ {n d : F},
        d ≠ 0 →
          W.toAffine.negAddY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (n / (P 2 * Q 2 * d)) =
            (n *
                    (n ^ 2 + W.a₁ * n * P 2 * Q 2 * d - W.a₂ * P 2 ^ 2 * Q 2 ^ 2 * d ^ 2 - P 0 * Q 2 ^ 2 * d ^ 2 -
                        Q 0 * P 2 ^ 2 * d ^ 2 -
                      P 0 * Q 2 ^ 2 * d ^ 2) +
                  P 1 * Q 2 ^ 3 * d ^ 3) /
                (P 2 * Q 2) ^ 3 /
              d ^ 3