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