feat(order/cover): The covering relation (#10676)
This defines `a ⋖ b` to mean that `a < b` and there is no element in between. It is generally useful, but in particular in the context of polytopes and successor orders.
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Co-authored-by: Grayson Burton <noobie365@gmail.com>
