Lemma latticedec_notgtle : ∏ (x y : X), ¬ latticedec_gt_so x y → Lle lat x y. Proof. intros x y H. induction (isdecrel_latticedec lat x y) as [H0 | H0]. + exact H0. + apply fromempty, H. exact H0. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.