Lemma isarchring_isarchrig {X : ring} (R : hrel X) : isbinophrel (X := rigaddabmonoid X) R → isarchring R → isarchrig (X := ringtorig X) R. Proof. intros Hop1 H. repeat split. - intros y1 y2 Hy. assert (X0 : R (y1 - y2)%ring 0%ring). abstract (apply (pr2 (isinvbinophrelgr X Hop1)) with y2 ; change BinaryOperations.op with (@BinaryOperations.op1 X) ; rewrite ringassoc1, ringlinvax1, ringlunax1, ringrunax1 ; exact Hy). generalize (isarchring_1 _ H _ X0). apply hinhfun. intros n. exists (pr1 n). abstract (rewrite <- (ringrunax1 _ (nattorig (pr1 n) * y1)%ring), <- (ringlinvax1 _ (nattorig (pr1 n) * y2)%ring), <- ringassoc1 ; apply (pr2 Hop1) ; rewrite <- ringrmultminus, <- ringldistr ; exact (pr2 n)). - apply isarchring_2. exact H. - intros x. generalize (isarchring_2 _ H (- x)%ring). apply hinhfun. intros n. exists (pr1 n). abstract (change 0%rig with (0%ring : X) ; rewrite <- (ringlinvax1 _ x) ; apply (pr2 Hop1) ; exact (pr2 n)). 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.