proposition: Lemma isassocquot {X : monoid} (R : binopeqrel X) : isassoc (@op (setwithbinopquot R)).
proof: Proof. intros a b c. apply (setquotuniv3prop R (λ x x' x'' : setwithbinopquot R, make_hProp _ (setproperty (setwithbinopquot R) (op (op x x') x'') (op x (op x' x''))))). intros x x' x''. apply (maponpaths (setquotpr R) (assocax X x x' x'')). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders