∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) (ha₁ : W.a₁ ≠ 0),
  W.toCharTwoJNeZeroNF ha₁ =
    { u := Units.mk0 W.a₁ ha₁, r := W.a₃ / W.a₁, s := 0, t := (W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) / W.a₁ ^ 3 }