Definition Lle_notLgt : ∏ x y : X, Lle lat x y → ¬ Lgt lat x y := λ x y : X, pr2 (pr1 (pr2 (pr2 lat)) x y).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.