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

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