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

State before:
m : ℕ
i : Fin (m + 1)
⊢ i.rev ≠ 0 ↔ i ≠ last m
Tactic:
simp_rw [ne_eq, rev_eq_zero_iff_last]
State after:
no goals