basic): Monotonicity of `nat.find_greatest` (#10507)

Commit

4 years ago

feat(data/nat/basic): Monotonicity of `nat.find_greatest` (#10507) This proves that `nat.find_greatest` is monotone in both arguments.

Author

YaelDillies

Parents