∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  W'.Nonsingular P =
    (W'.Equation P ∧
      (W'.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W'.a₂ * P 0 * P 2 ^ 2 + W'.a₄ * P 2 ^ 4) ≠ 0 ∨
        2 * P 1 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 3 ≠ 0 ∨
          W'.a₁ * P 0 * P 1 + 3 * W'.a₃ * P 1 * P 2 ^ 2 -
              (2 * W'.a₂ * P 0 ^ 2 * P 2 + 4 * W'.a₄ * P 0 * P 2 ^ 3 + 6 * W'.a₆ * P 2 ^ 5) ≠
            0))