∀ (R : Type u_2) {M : Type u_3} [inst : Semiring R] [inst_1 : Invertible 2] [inst_2 : Lattice M]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [IsOrderedAddMonoid M] (x y : M), x ⊓ y = ⅟2 • (x + y - |y - x|)