Definition latticedec_gt : latticewithgt X. Proof. exists (lattice_latticedec lat). exists latticedec_gt_so. split ; split. - apply latticedec_notgtle. - apply latticedec_lenotgt. - apply latticedec_gtmin. - apply latticedec_gtmax. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.