Lemma ispartbinophrel_Lle (X : abmonoid) (Y : @submonoid X) (lat : lattice X) (Hmin : ispartrdistr Y (Lmin lat) op) : ispartbinophrel Y (Lle lat). Proof. split. - intros a b c Yc. rewrite !(commax _ c). unfold Lle ; rewrite <- (Hmin _ _ (c,,Yc)). apply (maponpaths (λ x, op x _)). - intros a b c Yc. unfold Lle ; rewrite <- (Hmin _ _ (c,,Yc)). apply (maponpaths (λ x, op x _)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.