proposition: 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: 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.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups