fact: Definition isarchgr {X : abgr} (R : hrel X) := ∏ x y1 y2 : X, R y1 y2 -> ∃ n : nat, R (natmult n y1 + x)%addmonoid (natmult n y2).
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics