proposition: Lemma Lmin_case : ∏ (P : X → UU) (x y : X), P x → P y → P (Lmin lat x y).
proof: Proof. intros P x y Hx Hy. apply Lmin_case_strong ; intros _. - exact Hx. - exact Hy. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups