proposition: Lemma istrans_setquot_aux {X : abmonoid} (R : hrel X) : istrans R -> isbinophrel R -> istrans (setquot_aux R).
proof: Proof. intros Hr Hop. intros x y z. apply hinhfun2. intros (c1,Hc1) (c2,Hc2). exists (c1 + c2)%addmonoid. eapply Hr. rewrite <- assocax. apply (pr2 Hop). exact Hc1. rewrite assocax, (commax _ c1), <- !assocax. apply (pr2 Hop). exact Hc2. Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics