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