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