mathlib

9ecdd380 - chore(algebra/order/sub): generalize 2 lemmas (#9611)

chore(algebra/order/sub): generalize 2 lemmas (#9611) * generalize `lt_sub_iff_left` and `lt_sub_iff_right`; * use general lemmas in `data.real.ennreal`.