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

State before:
m : ℕ
i : Fin (m + 1)
⊢ i ≠ 0 ↔ i.rev ≠ last m
Tactic:
convert rev_rev i ▸ rev_ne_zero_iff_ne_last
State after:
no goals