Definition istrans_Lgt : istrans (Lgt lat) := istrans_isStrongOrder (Lgt lat).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.