∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R),
  W.polynomial =
    Polynomial.X ^ 2 + Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃) * Polynomial.X -
      Polynomial.C
        (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)