chore(data/fin): reorder file to group declarations (#6109)
The `data/fin` file has a lot of definitions and lemmas. This reordering groups declarations and places ones that do not rely on `fin` operations first, like order. No definitions or lemma statements have been changed. A minimal amount of proofs have been rephrased. No reformatting of style has been done. Section titles have been added.
This is useful in preparation for redefining `fin` operations (lean#527). Additionally, it allows for better organization for other refactors like making `pred` and `pred_above` total.
