Commit 2021-03-03 13:41 a852bf40

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.