proposition: 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: Proof. intros H x y. rewrite H, assocax, grlinvax, lunax, runax. apply iscomm_Lmax. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups