n m : ℕ
p : Fin (n + 1)
i : Fin (n + 2)
h : i ≤ ↑castSucc p
this : i ≤ ↑castSucc (last n)
⊢ predAbove p i = castPred i
n m : ℕ
p : Fin (n + 1)
i : Fin (n + 2)
h : i ≤ ↑castSucc p
⊢ predAbove p i = castPred i
have : i ≤ castSucc (last n) := h.trans p.le_last
no goals
n m : ℕ
p : Fin (n + 1)
i : Fin (n + 2)
h : i ≤ ↑castSucc p
this : i ≤ ↑castSucc (last n)
⊢ predAbove p i = castPred i
simp [predAbove, castPred, h.not_lt, this.not_lt]