Theorem: Fin.succAbove_le_succ (Controlbits/Fin.lean)

State before:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i ≤ i.succ
Tactic:
obtain h | h := succAbove_eq_castSucc_or_succ p i <;> rw [h]
State after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.succAbove i = i.castSucc
⊢ i.castSucc ≤ i.succ

State before:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.succAbove i = i.castSucc
⊢ i.castSucc ≤ i.succ
Tactic:
exact (castSucc_lt_succ _).le
State after:
no goals