Lemma Lmax_case_strong : ∏ (P : X → UU) (x y : X), (Lle lat y x → P x) → (Lle lat x y → P y) → P (Lmax lat x y). Proof. intros P x y Hx Hy. generalize (isdecrel_latticedec lat x y). apply sumofmaps ; intros H. - rewrite Lmax_le_eq_r. apply Hy, H. exact H. - enough (H0 : Lle lat y x). + rewrite Lmax_le_eq_l. apply Hx, H0. exact H0. + generalize (istotal_latticedec lat x y). apply hinhuniv, sumofmaps ; intros H0. apply fromempty, H, H0. exact H0. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.