Definition latticedec_gt_so : StrongOrder X. Proof. exists latticedec_gt_rel. repeat split. - apply istrans_latticedec_gt_rel. - apply iscotrans_latticedec_gt_rel. - intros x Hx. simple refine (Hx _). apply isrefl_Lle. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.