have := if_pos (lt i j)
  ((add 0 1).comp₂ _ (mul j j) (proj i))
  ((add 0 1).comp₂ _ ((add 0 1).comp₂ _ (mul i i) (proj i)) (proj j))
n : ℕ
i j : Fin n
⊢ Arith₁ fun v => (v.get i).pair (v.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
⊢ Arith₁ fun v => (v.get i).pair (v.get j)