mathlib3

b9cbf575 - feat(order/cover): Covering two distinct elements (#17274)

feat(order/cover): Covering two distinct elements (#17274) `a ⩿ c → b ⩿ c → a ≠ b → a ⊔ b = c` and dually. This is precisely one of the two Jordan-Hölder lattice laws when we set `is_maximal := (⋖)`.