have hpos : 0 < v.get i % v.get j - m := Nat.lt_sub_of_add_lt (by simpa using hm)
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
⊢ 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
⊢ False