Definition isarchrig {X : rig} (R : hrel X) := (∏ y1 y2 : X, R y1 y2 → ∃ n : nat, R (nattorig n * y1)%rig (1 + nattorig n * y2)%rig) × (∏ x : X, ∃ n : nat, R (nattorig n) x) × (∏ x : X, ∃ n : nat, R (nattorig n + x)%rig 0%rig).
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.