chore(order/cover): split to reduce imports

[semorrison]

This doesn't have a giant effect by itself, but if we also split order.atoms to separate out the material about fintype, we get more.

---

[YaelDillies]

This does not seem like a particularly pertinent split. I cannot see any theme among the lemmas you split off except that they are about covby. Can you move the ord_connected lemmas to data.set.intervals.ord_connected and leave the others where they are?

The only other idea I have is to split into order.cover.basic, order.cover.interval and order.cover.prod, but it's getting ridiculous for such a short file.

[semorrison]

The split is just "does this require all of finiteness or not".

[PatrickMassot]

bors d+

[bors]

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

Then your new file is misnamed 😅

[YaelDillies]

Let me put this on hold because:

• This specific split is unmotivated in my opinion
• move(data/set/pointwise/interval): Sanitise imports #17347 should supersede it

[PatrickMassot]

Yaël, this isn't an unmotivated split, it is motivated by the porting effort. Nothing can be a stronger motivation. However if your alternative modification is better for porting then of course we can consider it.