Definition Lmin_Lgt : ∏ x y z : X, Lgt lat x z → Lgt lat y z → Lgt lat (Lmin lat x y) z := pr1 (pr2 (pr2 (pr2 lat))).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.