Lemma truncminus_truncminus : ∏ x y, Lle lat 0 x → Lle lat x y → truncminus ex y (truncminus ex y x) = x. Proof. intros x y Hx Hxy. eapply rcancel. { apply is1. } simpl. erewrite (commax _ x), istruncminus_ex. refine (pathscomp0 _ _). apply istruncminus_ex. rewrite !Lmax_le_eq_l. - reflexivity. - exact Hxy. - apply truncminus_le. apply istrans_Lle with x. exact Hx. exact Hxy. exact Hx. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.