have : @Arith₁ (n + 1) (fun v => isLeNat v.head (v.tail.get j)) :=
  (le 0 1).comp₂ _ head ((proj j.succ).of_eq <| by simp)
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
⊢ Arith₁ fun v => (v.get i).isDvdNat (v.get j)
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
⊢ Arith₁ fun v => (v.get i).isDvdNat (v.get j)