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