proposition: Lemma truncminus_pos' : ∏ x y : X, Lgt lat (truncminus ex x y) 0 → Lgt lat x y.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups