Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-30 18:39 86c955eb

View on Github →

feat(data/nat): find_greatest is always bounded

Estimated changes

added theorem nat.find_greatest_le