Commit 2025-07-14 12:58 da48ff78

View on Github →

feat(Data/ENNReal): Add sub_lt_iff_lt_left and similar lemmas (#26815)

  • sub_lt_iff_lt_left
  • le_sub_iff_add_le_left
  • le_sub_iff_add_le_right

Estimated changes