Commit 2022-04-18 17:14 5c75390e
View on Github →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.