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

State before:
m : ℕ
i : Fin (m + 1)
⊢ 0 < i.rev ↔ i < last m
Tactic:
simp_rw [lt_last_iff_ne_last, pos_iff_ne_zero]
State after:
m : ℕ
i : Fin (m + 1)
⊢ i.rev ≠ 0 ↔ i ≠ last m

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