mathlib3
86493f12 - feat(data/nat): decidable exists le instance (#10857)

Commit

4 years ago

feat(data/nat): decidable exists le instance (#10857) Adds the `le` instance for a corresponding `lt` instance above.

Author

b-mehta

Parents