feat(order/bounds): ⨆ i, f i + g i ≤ ⨆ i, f i + ⨆ i, g i

[urkud]

We formulate this fact using is_lub because there is no typeclass
extending both ordered_add_comm_monoid and
complete_lattice.

---

[sgouezel]

I am afraid this formulation will not be as easy to use as it should be in the cases of interest (say ennreal). Can't you introduce a suitable typeclass making it possible to formalize it in a clean way?

(In the long run, I think it would be better to disentangle our typeclass hierarchy, by having a main hierarchy for algebra, a main hierarchy for orders, and then mixins saying how the two interact, but I remember a discussion on Zulip with Mario where he said he preferred to have zillions of classes, for a reason I didn't really get).

[urkud]

Which typeclass are you talking about? Just add_le_add?

Another way is to drop the lemmas and use the one-line proofs.

[sgouezel]

Depends on what you want to do with it. If you want to apply it in a typeclass extending ordered_add_comm_monoid and complete_lattice, then you can define such a typeclass, and show that the examples that are interesting to you are instances.