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