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