Lemma latticedec_gt_ge : ∏ x y : X, latticedec_gt_rel x y → Lge lat x y. Proof. intros x y Hxy. generalize (istotal_latticedec lat x y). apply hinhuniv, sumofmaps ; intros H. - apply fromempty. exact (Hxy H). - exact H. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.