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