Lemma truncminus_0_l_le0 : ∏ x : X, Lle lat x 0 → truncminus ex 0 x + x = 0. Proof. intros x Hx. rewrite istruncminus_ex. apply Lmax_le_eq_l, Hx. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.