mathlib
33a323cd - feat(data/fin): lemmas about ordering and cons (#13044)

Commit

3 years ago

feat(data/fin): lemmas about ordering and cons (#13044) This marks a few extra facts `simp`, since the analogous facts are `simp` for `nat`.

Author

eric-wieser

Parents