Lemma isequiv_setquot_aux {X : abmonoid} (R : hrel X) : isinvbinophrel R → ∏ x y : X, (setquot_aux R) x y <-> R x y. Proof. intros H x y. split. apply hinhuniv. intros (c,H'). generalize H'; clear H'. apply (pr2 H). intros H1. apply hinhpr. exists 0%addmonoid. rewrite !runax. exact H1. 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.