have hf : Arith₁ (fun v => isLtNat (v.get i - (v.get i).sqrt * (v.get i).sqrt) (v.get i).sqrt) :=
  (lt 0 1).comp₂ _
    ((Arith₁.sub 0 1).comp₂ _ (proj i) ((mul 0 1).comp₂ _ (Arith₁.sqrt i) (Arith₁.sqrt i)))
    (Arith₁.sqrt i)
n : ℕ
i : Fin n
⊢ Arith₁ fun v => (v.get i).unpair.1
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.1