mathlib3

4cf20164 - 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`.