Lemma istruncminus_ex {X : abmonoid} {lat : lattice X} (ex : extruncminus lat) : ∏ x y : X, truncminus ex x y + y = Lmax lat x y. Proof. apply (pr2 ex). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.