Lemma Lmin_Lbot (x : X) : Lmin l (Lbot l) x = Lbot l. Proof. now rewrite <- (islunit_Lmax_Lbot x), Lmin_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.