Lemma truncminus_le_l : ∏ k x y : X, Lle lat y x → Lle lat (truncminus ex k x) (truncminus ex k y). Proof. intros k x y H. apply (rcancel (is1 y)). rewrite is3, istruncminus_ex. apply (rcancel (is1 x)). rewrite is3, assocax, (commax _ y), <- assocax, istruncminus_ex. rewrite !is2, (commax _ y), <- is4, !(commax _ k), <- is3, H. reflexivity. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.