feat(order/grade): Graded orders (#11308)
Define graded orders. To be the most general, we use `is_min`/`is_max` rather than `order_bot`/`order_top`. A grade is a function that respects the covering relation and eventually minimality/maximality.
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Grayson Burton <ocornoc@protonmail.com>
Co-authored-by: Vladimir Ivanov @astOwOlfo
