Lemma Lmax_le_case : ∏ x y z : X, Lle lat x z → Lle lat y z → Lle lat (Lmax lat x y) z. Proof. intros x y z <- <-. set (w := Lmax _ (Lmin _ x z) (Lmin _ y z)). assert (c : z = (Lmax lat w z)). - unfold w. now rewrite isassoc_Lmax, (iscomm_Lmax _ (Lmin _ y z) _), (iscomm_Lmin _ y z), Lmax_absorb, iscomm_Lmax, iscomm_Lmin, Lmax_absorb. - rewrite c. use (Lmin_absorb lat). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.