Definition Lgt {X : hSet} (lat : latticewithgt X) : StrongOrder X := pr1 (pr2 lat).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.