Lemma Lmin_le_case : ∏ x y z : X, Lle lat z x → Lle lat z y → Lle lat z (Lmin lat x y). Proof. intros x y z <- <-. simpl. rewrite (iscomm_Lmin _ x), <- isassoc_Lmin. rewrite (isassoc_Lmin _ _ _ y), Lmin_id. rewrite isassoc_Lmin, (iscomm_Lmin _ y). rewrite isassoc_Lmin, <- (isassoc_Lmin _ x), Lmin_id. apply pathsinv0, isassoc_Lmin. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.