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