Lemma truncminus_le : ∏ x y : X, Lle lat 0 x → Lle lat 0 y → Lle lat (truncminus ex x y) x. Proof. intros x y Hx Hy. apply (op_le_r' _ is1 is3 y). rewrite istruncminus_ex. apply Lmax_le_case. - apply istrans_Lle with (0 + x). + rewrite (lunax _ x). apply isrefl_Lle. + rewrite (commax _ x). now apply op_le_r. - apply istrans_Lle with (0 + y). + rewrite (lunax _ y). apply isrefl_Lle. + now apply op_le_r. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.