refactor(data/nat/lattice): move code, add lemmas (#8708)
* move `nat.conditionally_complete_linear_order_with_bot` and `enat.complete_linear_order` to a new file `data.nat.lattice`;
* add a few lemmas (`nat.supr_lt_succ` etc), move `set.bUnion_lt_succ` to the same file;
* use `galois_insertion.lift_complete_lattice` to define `enat.complete_linear_order`.
