Lemma truncminus_0_l_ge0 : ∏ x : X, Lle lat 0 x → truncminus ex 0 x = 0. Proof. intros x Hx. apply truncminus_eq_0, Hx. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.