proposition: Lemma Lmin_case_strong : ∏ (P : X → UU) (x y : X), (Lle lat x y → P x) → (Lle lat y x → P y) → P (Lmin lat x y).
proof: Proof. intros P x y Hx Hy. generalize (isdecrel_latticedec lat x y). apply sumofmaps ; intros H. - rewrite Lmin_le_eq_l. apply Hx, H. exact H. - enough (H0 : Lle lat y x). + rewrite Lmin_le_eq_r. apply Hy, H0. exact H0. + generalize (istotal_latticedec lat x y). apply hinhuniv, sumofmaps ; intros H0. apply fromempty, H, H0. exact H0. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups