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

State before:
m : ℕ
i : Fin m
⊢ i.castSucc.rev.castSucc = i.succ.rev.succ
Tactic:
simp_rw [rev_succ, rev_castSucc, succ_castSucc]
State after:
no goals