proposition: Lemma Lmin_Lbot (x : X) : Lmin l (Lbot l) x = Lbot l.
proof: Proof. now rewrite <- (islunit_Lmax_Lbot x), Lmin_absorb. Qed.
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Propositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.OrderTheory.Lattice.Lattice