Lemma istrans_Lge : istrans (Lge lat). Proof. intros x y z Hxy Hyz. apply (istrans_Lle lat) with y. exact Hyz. exact Hxy. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.