Definition Lmin_ge_case : ∏ (x y z : X), Lge lat x z → Lge lat y z → Lge lat (Lmin lat x y) z := Lmin_le_case lat.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.