feat(data/equiv/fin): fin_add_flip and fin_rotate (#6454)
Add
* `fin_add_flip : fin (m + n) ≃ fin (n + m)`
* `fin_rotate : Π n, fin n ≃ fin n` (acts by +1 mod n)
and simp lemmas, and shows `fin.snoc` is a rotation of `fin.cons`.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
