simp only [Bool.or_eq_false_eq_eq_false_and_eq_false,
  decide_eq_false_iff_not, Bool.and_eq_false_eq_eq_false_or_eq_false, not_lt]
case right
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
m : ℕ
hm : m < v.get i - v.get j
⊢ (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0)) = false
case right
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
m : ℕ
hm : m < v.get i - v.get j
⊢ ¬m + v.get j = v.get i ∧ (v.get j ≤ v.get i ∨ ¬m = 0)