Lemma isPartialOrder_Lle : isPartialOrder (Lle lat). Proof. split ; [ split | ]. - exact istrans_Lle. - exact isrefl_Lle. - exact isantisymm_Lle. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.