simp only [head_cons, get_cons_succ, or_pos_iff, isEqNat_pos_iff, and_pos_iff,
  isLtNat_pos_iff, Bool.decide_or, Bool.decide_and, PFun.coe_val, eq_some_iff, mem_rfind,
  mem_some_iff, F]
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
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.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ true =
      (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0)) ∧
    ∀ {m : ℕ},
      m < v.get i - v.get j → false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))