Lemma istrans_setquot_aux {X : abmonoid} (R : hrel X) : istrans R → isbinophrel R → istrans (setquot_aux R). 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.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.DivisionRig. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.ConstructiveStructures. Require Import UniMath.MoreFoundations.Tactics.