Lemma istrans_Lge_Lgt : ∏ x y z : X, Lge lat x y → Lgt lat y z → Lgt lat x z. Proof. intros x y z Hge Hgt. generalize (iscotrans_Lgt _ x _ Hgt). apply hinhuniv. apply sumofmaps ; intros H. - apply fromempty. refine (Lle_notLgt _ _ _ _). exact Hge. exact H. - exact H. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.