refactor(order/complete_lattice): Sup lemmas before Inf lemmas (#…

…14868)

Throughout the file, we make sure that `Sup` theorems always appear immediately before their `Inf` counterparts. This ensures consistency, and makes it much easier to golf theorems or detect missing API.

We choose to put `Sup` before `Inf` rather than the other way around, since this seems to minimize the amount of things that need to be moved around, and it matches the order that we define the two operations.

We also golf a few proofs throughout, and add some missing corresponding theorems, namely:
- `infi_extend_top`
- `infi_supr_ge_nat_add`
- `unary_relation_Inf_iff`
- `binary_relation_Inf_iff`



Co-authored-by: YaelDillies <yael.dillies@gmail.com>