Closed DyeKuu closed 2 years ago
Note:
The current formalization by me is only a necessary condition. It covers only the half part of https://leanprover-community.github.io/mathlib_docs/order/bounds.html#is_greatest.
Either we stick to current formalization and add another one saying that 112 meets all the requirements, either we use is_greatest. I choose here the latter plan.
is_greatest
Note:
The current formalization by me is only a necessary condition. It covers only the half part of https://leanprover-community.github.io/mathlib_docs/order/bounds.html#is_greatest.
Either we stick to current formalization and add another one saying that 112 meets all the requirements, either we use
is_greatest. I choose here the latter plan.