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