have hr : @Arith₁ (n + 1) (fun v =>
  (isEqNat (v.head * (v.get i.succ)) (v.get j.succ)).or (isLtNat (v.get j.succ) v.head)) :=
  (or 0 1).comp₂ _
    ((equal 0 1).comp₂ _ ((mul 0 1).comp₂ _ head (proj i.succ)) (proj j.succ))
    ((lt 0 1).comp₂ _ (proj j.succ) head)
n : ℕ
i j : Fin n
⊢ 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)
⊢ Arith₁ fun v => (v.get i).isDvdNat (v.get j)