Lemma truncminus_pos' : ∏ x y : X, Lgt lat (truncminus ex x y) 0 → Lgt lat x y. Proof. intros x y Hgt. apply (is0 y) in Hgt. rewrite istruncminus_ex, lunax in Hgt. rewrite <- (Lmax_le_eq_l lat x y). exact Hgt. apply notLgt_Lle. intros H ; revert Hgt. apply Lle_notLgt. rewrite Lmax_le_eq_r. apply isrefl_Lle. apply Lgt_Lge. exact H. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.