Definition isarchrig_gt {X : rig} (R : hrel X) : isarchrig R → ∏ x : X, ∃ n : nat, R (nattorig n) x := λ H, (pr1 (pr2 H)).
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.