simp [F, Part.eq_some_iff, Nat.dvd_sub_mod]
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
⊢ (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) = (↑fun v => v.get i % v.get j) v
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 : ℕ}, m < v.get i % v.get j → ¬v.get j ∣ v.get i - m