proposition: Lemma isarchrig_setquot_aux {X : rig} (R : hrel X) : isinvbinophrel (X := rigaddabmonoid X) R → isarchrig R → isarchrig (setquot_aux (X := rigaddabmonoid X) R).
proof: Proof. intros Hr H. split ; [ | split]. - intros y1 y2. apply hinhuniv. intros Hy. generalize (isarchrig_diff R H y1 y2 (pr2 Hr _ _ _ (pr2 Hy))). apply hinhfun. intros n. exists (pr1 n). apply hinhpr. exists 0%rig. rewrite runax, runax. exact (pr2 n). - intros x. generalize (isarchrig_gt R H x). apply hinhfun. intros n. exists (pr1 n). apply hinhpr. exists 0%rig. rewrite runax, runax. exact (pr2 n). - intros x. generalize (isarchrig_pos R H x). apply hinhfun. intros n. exists (pr1 n). apply hinhpr. exists 0%rig. rewrite runax, runax. exact (pr2 n). 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