∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Nonsingular P →
    WeierstrassCurve.Projective.Point.toAffine W (W.neg P) = -WeierstrassCurve.Projective.Point.toAffine W P