proposition: Lemma Lmax_id : ∏ x : X, Lmax lat x x = x.
proof: Proof. intros x. intermediate_path (Lmax lat x (Lmin lat x (Lmax lat x x))). - apply maponpaths, pathsinv0, Lmin_absorb. - apply Lmax_absorb. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups