Lemma isaprop_islatticeop {X : hSet} (min max : binop X) : isaprop (islatticeop min max). Proof. apply isapropdirprod ; [ | apply isapropdirprod] ; apply isapropdirprod. apply isapropisassoc. apply isapropiscomm. apply isapropisassoc. apply isapropiscomm. apply isapropisabsorb. apply isapropisabsorb. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.