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