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