rw[Nat.sub_eq_iff_eq_add (Nat.sub_le_sub_left (le_of_lt hm) _), Nat.sub_eq_iff_eq_add (le_of_lt hmvi),
  ←Nat.sub_add_comm (le_of_lt hm), Nat.add_sub_of_le (Nat.mod_le (v.get i) (v.get j)),
  Nat.sub_add_cancel (le_of_lt hmvi)]
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
⊢ v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m
no goals