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

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