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