Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-10 21:01 14a1fd7b

View on Github →

feat(data/nat/basic): le_of_add_le_* (#6145)

Estimated changes

Modified src/data/nat/basic.lean

added theorem nat.le_of_add_le_left

added theorem nat.le_of_add_le_right

Modified src/data/real/nnreal.lean

added theorem nnreal.le_of_add_le_left

added theorem nnreal.le_of_add_le_right