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