rcases this with (hv | hv)
case left
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
this : v.get i < v.get j ∨ v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
case left.inl
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
hv : v.get i < v.get j
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0

case left.inr
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
hv : v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0