apply Order.trans
case step
α : 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] ≤ arr[m✝.succ]
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

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
⊢ ?step.y ≤ arr[m✝.succ]

case step.y
α : 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
⊢ α