have : Arith₁ F :=
  (dvd 0 1).comp₂ _ (proj j.succ) ((sub 0 1).comp₂ _ (proj i.succ) head)
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
⊢ Arith₁ fun v => v.get i % v.get j
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
⊢ Arith₁ fun v => v.get i % v.get j