Lemma truncminus_ge_0 : ∏ x y : X, Lle lat 0 (truncminus ex x y). Proof. intros x y. apply (op_le_r' _ is1 is3 y). rewrite istruncminus_ex, lunax. apply Lmax_ge_r. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.