feat(order/cover): Covering elements are unique (#14156)
feat(order/cover): Covering elements are unique (#14156)

In a linear order, there's at most one element covering `a` and at most one element being covered by `a`.





leanprover-community/mathlib,leanprover-community/mathlib