mathlib3

5c75390e - feat(data/real/ennreal): Order properties of addition (#13371)

feat(data/real/ennreal): Order properties of addition (#13371) Inherit algebraic order lemmas from `with_top`. Also protect `ennreal.add_lt_add_iff_left` and `ennreal.add_lt_add_iff_right`, as they should have been.