n✝ m n i : ℕ
h : i < n + 1
this : ¬↑castSucc (last n) < { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
⊢ castPred { val := i, isLt := (_ : i < Nat.succ (n + 1)) } = { val := i, isLt := h }
n✝ m n i : ℕ
h : i < n + 1
⊢ castPred { val := i, isLt := (_ : i < Nat.succ (n + 1)) } = { val := i, isLt := h }
have : ¬castSucc (last n) < ⟨i, lt_succ_of_lt h⟩ := by
  simpa [lt_iff_val_lt_val] using le_of_lt_succ h
no goals
n✝ m n i : ℕ
h : i < n + 1
this : ¬↑castSucc (last n) < { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
⊢ castPred { val := i, isLt := (_ : i < Nat.succ (n + 1)) } = { val := i, isLt := h }
simp [castPred, predAbove, this]
no goals
n✝ m n i : ℕ
h : i < n + 1
⊢ ¬↑castSucc (last n) < { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
simpa [lt_iff_val_lt_val] using le_of_lt_succ h