Lemma isarchrig_setquot_aux {X : rig} (R : hrel X) : isinvbinophrel (X := rigaddabmonoid X) R → isarchrig R → isarchrig (setquot_aux (X := rigaddabmonoid X) R). 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.
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.