by_cases hv : v i < v j <;> simp[hv, Nat.isLtNat, eq_comm]
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i j : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ v i < v j ∧ y = 1 ∨ v j ≤ v i ∧ y = 0 ↔ (v i).isLtNat (v j) = y
case neg
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i j : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
hv : ¬v i < v j
⊢ y = 0 → v j ≤ v i