Definition islatticewithgtrel {X : hSet} (lat : lattice X) (gt : StrongOrder X) := (∏ x y : X, (¬ (gt x y)) <-> Lle lat x y) × (∏ x y z : X, gt x z → gt y z → gt (Lmin lat x y) z) × (∏ x y z : X, gt z x → gt z y → gt z (Lmax lat x y)).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.