proposition: Lemma ispartbinophrel_Lle (X : abmonoid) (Y : @submonoid X) (lat : lattice X) (Hmin : ispartrdistr Y (Lmin lat) op) : ispartbinophrel Y (Lle lat).
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups