Lemma truncminus_Lmin_l : ∏ k x y : X, truncminus ex (Lmin lat x y) k = Lmin lat (truncminus ex x k) (truncminus ex y k). Proof. intros k x y. eapply rcancel. { apply (is1 k). } simpl. rewrite is3, 2!istruncminus_ex. apply (pathscomp0 (istruncminus_ex _ _ _)). apply is4. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.