Definition istruncminus {X : abmonoid} (lat : lattice X) (minus : binop X) := ∏ x y : X, minus x y + y = Lmax lat x y.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.