[ new ] Fin n as a refinement

[gallais]

This version has a better runtime representation
This version lets us have efficient implementations of things like splitAt and quotRem

I have been using this definition in my https://github.com/gallais/agda-tiling DSL and
it makes the library a lot faster.

I almost have feature parity with Data.Fin.Base (I have not implemented e.g. punchOut).

[jamesmckinna]

I think that this all looks great (but see also #2257 and #2292 which took a different angle of attack, focusing on modular arithmetic), but I'm a bit concerned about like-for-like emulation of the existing Data.Fin.Base API, when there are still many open issues drawing attention to... things which could be improved there. So I'm not sure I'd want to saddle us with the maintenance headache of fixing those issues on the new additions.

Also: where does this leave us wrt the 'propaganda' for DTFP with eg using Fin for type-safe/bounds-safe Data.Vec.Base.lookup?

[jamesmckinna]

This all looks fine; lots of potential downstream uses/improvements, but worth landing this sooner rather than later.

[jamesmckinna]

@gallais do you want this badged for v2.4?

[gallais]

I am in no rush but also happy to see it included. I have a deadline today but should be able to have
a look (and merge your proposals; glad the sniping worked!) later this week.

[jamesmckinna]

Nice cleanup operation!

[JacquesCarette]

A few nitpicks and one issue with naming. Otherwise, this looks great.

I believe this is also now the definition that 1lab uses.

[jamesmckinna]

Maybe punchOut etc. could/should better follow the example of Data.List.Base.filter etc. and use Decidable _<_ as the engine of case analysis?