Lemma truncminus_pos : ∏ x y : X, Lgt lat x y → Lgt lat (truncminus ex x y) 0. Proof. intros x y. intros H. apply (is1 y). rewrite lunax, istruncminus_ex. rewrite Lmax_le_eq_l. exact H. apply Lgt_Lge, H. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.