intro v
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
⊢ ∀ (i_1 : Vector ℕ n),
    (if 0 < (i_1.get i).isLtNat (i_1.get j) then i_1.get j * i_1.get j + i_1.get i
      else i_1.get i * i_1.get i + i_1.get i + i_1.get j) =
      (i_1.get i).pair (i_1.get j)
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)