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