Lemma Lmax_case : ∏ (P : X → UU) (x y : X), P x → P y → P (Lmax lat x y). Proof. intros P x y Hx Hy. apply Lmax_case_strong ; intros _. - exact Hx. - exact Hy. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.