Definition isarchring {X : ring} (R : hrel X) := (∏ x : X, R x 0%ring → ∃ n : nat, R (nattoring n * x)%ring 1%ring) × (∏ x : X, ∃ n : nat, R (nattoring n) x).
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.