Lemma truncminus_0_r : ∏ x : X, truncminus ex x 0 = Lmax lat x 0. Proof. intros x. rewrite <- (runax _ (truncminus _ _ _)). apply (istruncminus_ex). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.