theorem absorb1 {α : Type u_1} [Lattice α] (x : α) (y : α) : x ⊓ (x ⊔ y) = x

theorem absorb2 {α : Type u_1} [Lattice α] (x : α) (y : α) : x ⊔ x ⊓ y = x