Some recursive Fin functions

[dolio]

Adds Fin to ℕ and a generalized version of ℕ to Fin (using _<_ rather than just successor).

I found myself needing these when using these as variables in well-scoped lambda terms.

[mortberg]

Looks good to me, but why use the recursive Fin instead of the one in Fin.Base?

[dolio]

I find the recursive Fin better to use in most situations. The other one uses k + m = n ordering, and with cubical paths, this does nothing to rule out impossible pattern matching cases.

[mortberg]

I find the recursive Fin better to use in most situations. The other one uses k + m = n ordering, and with cubical paths, this does nothing to rule out impossible pattern matching cases.

Ok, it's a bit unfortunate that we have 3 different Fin's in the library which are in use... It could be nice to have only one and develop all the theory once and for all instead of three times...