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