exact (ArithPart₁.rfindPos this).of_eq <| by
  intro v; simp [F, Part.eq_some_iff, Nat.dvd_sub_mod]
  intro m hm A
  have hmvi : m < v.get i := lt_of_lt_of_le hm <| Nat.mod_le (v.get i) (v.get j)
  have hsub : v.get j ∣ v.get i % v.get j - m := by
    have : v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m := by
      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)]
    rw[←this]
    exact Nat.dvd_sub (Nat.sub_le_sub_left (le_of_lt hm) _) A (@Nat.dvd_sub_mod (v.get j) (v.get i))
  have hpos : 0 < v.get i % v.get j - m := Nat.lt_sub_of_add_lt (by simpa using hm)
  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
  have : ¬v.get j ∣ v.get i % v.get j - m := Nat.not_dvd_of_pos_of_lt hpos this
  contradiction
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
no goals