case h
n m : ℕ
x y : Fin (n + 1)
h : x < y
hx : optParam (↑x < n) (_ : ↑x < n)
⊢ ↑castSucc (castLT x hx) < y
n m : ℕ
x y : Fin (n + 1)
h : x < y
hx : optParam (↑x < n) (_ : ↑x < n)
⊢ ↑(succAbove y) (castLT x hx) = x
rw [succAbove_below, castSucc_castLT]
no goals
case h
n m : ℕ
x y : Fin (n + 1)
h : x < y
hx : optParam (↑x < n) (_ : ↑x < n)
⊢ ↑castSucc (castLT x hx) < y
exact h