proposition: Lemma isbinophrel_setquot_aux {X : abmonoid} (R : hrel X) : isbinophrel R -> isbinophrel (setquot_aux R).
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics