Lemma truncminus_eq_0 : ∏ x y : X, Lle lat x y → truncminus ex x y = 0. Proof. intros x y H. eapply rcancel. { apply is1. } simpl. refine (pathscomp0 _ _). apply istruncminus_ex. refine (pathscomp0 _ _). apply Lmax_le_eq_r, H. apply pathsinv0, (lunax X). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.