Lemma isbinophrel_setquot_aux {X : abmonoid} (R : hrel X) : isbinophrel R → isbinophrel (setquot_aux R). Proof. intros Hop. split. - intros x y z. apply hinhfun. intros (c,Hc). exists c. rewrite !assocax. apply (pr1 Hop). exact Hc. - intros x y z. apply hinhfun. intros (c,Hc). exists c. rewrite !assocax, (commax _ z), <- !assocax. apply (pr2 Hop). exact Hc. 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.