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