proposition: Lemma istrans_Lge_Lgt : ∏ x y z : X, Lge lat x y → Lgt lat y z → Lgt lat x z.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups