Lemma isarchrig_isarchring {X : ring} (R : hrel X) : isbinophrel (X := rigaddabmonoid X) R → isarchrig (X := ringtorig X) R → isarchring R. Proof. intros Hr H. split. - intros x Hx. generalize (isarchrig_diff _ H _ _ Hx). apply hinhfun. intros (n,Hn). exists n. rewrite <- (ringrunax1 _ 1%ring), <- (ringmultx0 _ (nattoring n)). exact Hn. - apply (isarchrig_gt (X := ringtorig X)). exact H. 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.