Lemma truncminus_Lmax_r : ∏ (k x y : X), Lle lat (Lmin lat (y + y) (x + x)) (x + y) → truncminus ex k (Lmax lat x y) = Lmin lat (truncminus ex k x) (truncminus ex k y). Proof. intros k x y H. eapply rcancel. { apply is1. } rewrite is3, istruncminus_ex. rewrite !(commax _ _ (Lmax _ _ _)), !is2. rewrite !(commax _ _ (truncminus _ _ _)), !istruncminus_ex. rewrite (iscomm_Lmax _ (_*_)%multmonoid (Lmax _ _ _)). rewrite !isassoc_Lmax, !(iscomm_Lmax _ k). rewrite <- is4. eapply rcancel. { apply is1. } rewrite !is2, is3, !is2. rewrite assocax, (commax _ y x), <- assocax. rewrite istruncminus_ex, is2. eapply rcancel. { apply (is1 y). } rewrite !is2, is3, !is2. rewrite !assocax, (commax _ (truncminus _ _ _)), !assocax, (commax _ _ (truncminus _ _ _)). rewrite istruncminus_ex. rewrite (commax _ _ (Lmax _ _ _)), is2. rewrite (commax _ _ (Lmax _ _ _)), is2. rewrite 4!(commax _ _ x). rewrite <- (isassoc_Lmax _ _ _ (x * (y * y))%multmonoid). rewrite (iscomm_Lmax _ (x * (y * y))%multmonoid (Lmax _ _ _)). rewrite <- is4. rewrite (iscomm_Lmax _ (x * (x * y))%multmonoid (k * (y * y))%multmonoid), <- is4. rewrite !(commax _ k), <- !assocax. rewrite <- is3. rewrite !(iscomm_Lmax _ _ (x * y * k)%multmonoid), <- !isassoc_Lmax. rewrite (Lmax_le_eq_l _ (x * y * k)%multmonoid (Lmin lat (y * y) (x * x) * k)%multmonoid). reflexivity. apply op_le_r. exact is3. exact H. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.