feat(data/fin): refactor pred_above (#6125)

Currently the signature of `pred_above` is
```lean
def pred_above (p : fin (n+1)) (i : fin (n+1)) (hi : i ≠ p) : fin n := ...
```
and its behaviour is "subtract one from `i` if it is greater than `p`".

There are two reasons I don't like this much:
1. It's not a total function.
2. Since `succ_above` is exactly a simplicial face map, I'd like `pred_above` to be a simplicial degeneracy map.

In this PR I propose replacing this with
```lean
def pred_above (p : fin n) (i : fin (n+1)) : fin n :=
```
again with the behaviour "subtract one from `i` if it is greater than `p`".

~~Unfortunately, it seems the current `pred_above` really is needed for the sake of `fin.insert_nth`, so this PR has ended up as a half-hearted attempt to replace `pred_above` 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: 3 people