Lemma iscommquot {X : abmonoid} (R : binopeqrel X) : iscomm (@op (setwithbinopquot R)). Proof. intros. set (X0 := setwithbinopquot R). intros x x'. apply (setquotuniv2prop R (λ x x' : X0, make_hProp _ (setproperty X0 (x + x') (x' + x)))). intros x0 x0'. apply (maponpaths (setquotpr R) ((commax X) x0 x0')). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.