∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P Q : Fin 3 → R),
  W'.negAddY P Q =
    -3 * P 0 ^ 2 * Q 0 * Q 1 + 3 * P 0 * Q 0 ^ 2 * P 1 - P 1 ^ 2 * Q 1 * Q 2 + P 1 * Q 1 ^ 2 * P 2 +
                                W'.a₁ * P 0 * Q 1 ^ 2 * P 2 -
                              W'.a₁ * Q 0 * P 1 ^ 2 * Q 2 -
                            W'.a₂ * P 0 ^ 2 * Q 1 * Q 2 +
                          W'.a₂ * Q 0 ^ 2 * P 1 * P 2 +
                        2 * W'.a₂ * P 0 * Q 0 * P 1 * Q 2 -
                      2 * W'.a₂ * P 0 * Q 0 * Q 1 * P 2 -
                    W'.a₃ * P 1 ^ 2 * Q 2 ^ 2 +
                  W'.a₃ * Q 1 ^ 2 * P 2 ^ 2 +
                W'.a₄ * P 0 * P 1 * Q 2 ^ 2 -
              2 * W'.a₄ * P 0 * Q 1 * P 2 * Q 2 +
            2 * W'.a₄ * Q 0 * P 1 * P 2 * Q 2 -
          W'.a₄ * Q 0 * Q 1 * P 2 ^ 2 +
        3 * W'.a₆ * P 1 * P 2 * Q 2 ^ 2 -
      3 * W'.a₆ * Q 1 * P 2 ^ 2 * Q 2