Lemma iscotrans_latticedec_gt_rel : iscotrans latticedec_gt_rel. Proof. intros x y z Hxz. induction (isdecrel_latticedec lat x y) as [Hxy | Hyx]. - apply hinhpr, ii2. intros Hyz. simple refine (Hxz _). apply istrans_Lle with y. exact Hxy. exact Hyz. - apply hinhpr, ii1. exact Hyx. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.