∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      ∀ {u v : F},
        u ≠ 0 →
          v ≠ 0 → WeierstrassCurve.Jacobian.addU (u • P) (v • Q) = (u * v) ^ 2 * WeierstrassCurve.Jacobian.addU P Q