Lemma abgr_truncminus {X : abgr} (lat : lattice X) : isrdistr (Lmax lat) op → istruncminus (X := abgrtoabmonoid X) lat (λ x y : X, Lmax lat 0 (x + grinv X y)). Proof. intros H x y. rewrite H, assocax, grlinvax, lunax, runax. apply iscomm_Lmax. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.