∀ {F : Type u_1} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] (x x_1 x_2 : W.Point),
  WeierstrassCurve.Affine.Point.toClass (x + x_1 + x_2) = WeierstrassCurve.Affine.Point.toClass (x + (x_1 + x_2))