Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.sub_le_right_iff_le_add

Modification history

2021-10-09 04:58
src/data/nat/basic.lean
refactor(data/nat/basic): finish removing sub lemmas (#9601) …
Deleted nat.sub_le_right_iff_le_addView on Github →
2018-09-29 07:48
data/nat/basic.lean
feat(data/nat/basic): remove superfluous assumptions
Modified nat.sub_le_right_iff_le_addView on Github →
2017-11-22 05:33
data/nat/basic.lean
refactor(data/finset): redefine finsets as subtype of multisets
Modified nat.sub_le_right_iff_le_addView on Github →
2017-09-17 15:38
data/nat/basic.lean
feat(data/nat): better sqrt + pairing, prime numbers, renames...
Added nat.sub_le_right_iff_le_addView on Github →