feat(data/fin): fin n.succ is an add_comm_group (#6898)
This just moves the proof out of `data.zmod` basic.
Moving the full ring instance is left for future work, as `modeq`, used to prove left_distrib, is not available to import in `data/fin/basic`.
Note this adds an import of `data.int.basic` to `data.fin.basic`. I think this is probably acceptable?
