Lemma Lmax_Ltop (x : X) : Lmax l (Ltop l) x = Ltop l. Proof. now rewrite <- (islunit_Lmin_Ltop x), Lmax_absorb. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.OrderTheory.Lattice.Lattice.