proposition: Lemma isPartialOrder_Lge : isPartialOrder (Lge lat).
proof: Proof. split ; [ split | ]. - exact istrans_Lge. - exact isrefl_Lge. - exact isantisymm_Lge. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups