Assumptions `[semilattice_sup α] [is_total α (≤)]`

Stream: general

[Yury G. Kudryashov]

In #11218 I add a few lemmas to data.set.intervals.basic, and one of the new lemmas use assumptions [semilattice_sup α] [is_total α (≤)] (same as the other lemmas in the same section). @Yaël Dillies suggests that we rewrite all these lemmas in terms of [linear_order α]. Are there any use cases when we want these lemmas before we have [linear_order α]?

[Yury G. Kudryashov]

Mathematically, a partial order with [is_total α (≤)] is a linear order, see docs#as_linear_order, but there may be some technical reasons to have these strange assumptions. If not, then I'll migrate lemmas as suggested.