have : v.get i % v.get j - m < v.get j := by
  have : v.get i % v.get j < v.get j :=
    Nat.mod_lt _ (Nat.pos_of_ne_zero $ fun h => (Nat.not_lt.mpr (by simpa [Nat.sub_eq_zero_iff_le, h] using hsub)) hmvi)
  exact lt_of_le_of_lt (sub_le _ _) this
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
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
⊢ False
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
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
this : v.get i % v.get j - m < v.get j
⊢ False