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