∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Nonsingular P →
    P 2 ≠ 0 →
      Q 2 ≠ 0 →
        P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
          P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3 → W.dblU P ≠ 0