exact ih (Nat.lt_of_le_of_lt (Nat.le_succ ..) kn)
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[j] ≤ ?step.y
no goals