proposition: Lemma isantisymm_Lle : isantisymm (Lle lat).
proof: Proof. intros x y Hxy Hyx. apply pathscomp0 with (1 := pathsinv0 Hxy). apply pathscomp0 with (2 := Hyx). apply iscomm_Lmin. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups