proposition: 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: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics