Definition isarchmonoid {X : abmonoid} (R : hrel X) := ∏ x y1 y2 : X, R y1 y2 → (∃ n : nat, R (natmult n y1 + x)%addmonoid (natmult n y2)) × (∃ n : nat, R (natmult n y1) (natmult n y2 + x)%addmonoid).
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.