proposition: Lemma Lmin_le_case : ∏ x y z : X, Lle lat z x → Lle lat z y → Lle lat z (Lmin lat x y).
proof: Proof. intros x y z <- <-. simpl. rewrite (iscomm_Lmin _ x), <- isassoc_Lmin. rewrite (isassoc_Lmin _ _ _ y), Lmin_id. rewrite isassoc_Lmin, (iscomm_Lmin _ y). rewrite isassoc_Lmin, <- (isassoc_Lmin _ x), Lmin_id. apply pathsinv0, isassoc_Lmin. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups