proposition: Lemma isarchrig_isarchring {X : ring} (R : hrel X) : isbinophrel (X := rigaddabmonoid X) R -> isarchrig (X := ringtorig X) R -> isarchring R.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics