Lemma truncminus_Lmax_l : ∏ (k x y : X), truncminus ex (Lmax lat x y) k = Lmax lat (truncminus ex x k) (truncminus ex y k). Proof. intros k x y. apply (rcancel (is1 k)). rewrite is2, !istruncminus_ex. rewrite !isassoc_Lmax, (iscomm_Lmax _ k), isassoc_Lmax, Lmax_id. reflexivity. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.