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