chore(data/list/basic): streamline imports (#17616)
From the imports of `data.nat.order.basic`: Remove `data.set.basic`, by moving four lemmas to `data.nat.order.lemmas`.
From the imports of `data.list.basic`: Remove `algebra.order.with_zero` and `data.set.function` and downgrade `data.nat.order.lemmas` to `data.nat.order.basic`, by moving four lemmas to a new file `data.list.lemmas` and re-wording a couple of proofs.
