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