with_top max/sup diamond

Stream: general

[Yury G. Kudryashov]

There are two versions of sup on with_top α if α is a linear order. One comes from docs#with_top.semilattice_sup and the other one comes from docs#lattice_of_linear_order and docs#with_top.linear_order. This is why, e.g., docs#ennreal.sup_eq_max is not a rfl. What should we do? Add max/min to the signature of linear_order with default values?