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