Theorem isarchrigtoring : ∏ (X : rig) (R : hrel X) (Hr : R 1%rig 0%rig) (Hadd : isbinophrel (X := rigaddabmonoid X) R) (Htra : istrans R) (Harch : isarchrig (setquot_aux (X := rigaddabmonoid X) R)), isarchring (X := rigtoring X) (rigtoringrel X Hadd). Proof. intros. apply isarchgr_isarchring. abstract (apply hinhpr ; simpl ; exists 0%rig ; rewrite !rigrunax1 ; exact Hr). now apply (istransabgrdiffrel (rigaddabmonoid X)). now generalize Hadd ; apply isbinopabgrdiffrel. apply (isarchabgrdiff (X := rigaddabmonoid X)). exact Htra. apply isarchrig_isarchmonoid. abstract (apply hinhpr ; simpl ; exists 0%rig ; rewrite !rigrunax1 ; exact Hr). (now apply (istrans_setquot_aux (X := rigaddabmonoid X))). (now apply (isbinophrel_setquot_aux (X := rigaddabmonoid X))). exact Harch. Defined.
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.