induction jk with
| refl => exact Order.refl
| step h ih =>
  apply Order.trans
  . exact ih (Nat.lt_of_le_of_lt (Nat.le_succ ..) kn)
  . apply assms
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k : Nat
kn : k < n
jk : j ≤ k
⊢ arr[j] ≤ arr[k]
no goals