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