Definition isasymm_Lgt : isasymm (Lgt lat) := isasymm_isStrongOrder (Lgt lat).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.