simp[pair]
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
v : Vector ℕ n
⊢ (if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j) =
    (v.get i).pair (v.get j)
no goals