proposition: Lemma iscotrans_latticedec_gt_rel : iscotrans latticedec_gt_rel.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups