Lemma isarchmonoid_isarchrig {X : rig} (R : hrel X) : (R 1%rig 0%rig) → isarchmonoid (X := rigaddabmonoid X) R → isarchrig R. Proof. intros H01 H. repeat split. - intros y1 y2 Hy. generalize (isarchmonoid_2 _ H 1%rig y1 y2 Hy). apply hinhfun. intros n. exists (pr1 n). abstract (rewrite !nattorig_natmult, rigcomm1 ; exact (pr2 n)). - intros x. generalize (isarchmonoid_2 _ H x _ _ H01). apply hinhfun. intros n. exists (pr1 n). abstract ( pattern x at 1; rewrite <- (riglunax1 X x) ; pattern (0%rig : X) at 1; rewrite <- (rigmultx0 X (nattorig (pr1 n))) ; rewrite nattorig_natmult ; exact (pr2 n)). - intros x. generalize (isarchmonoid_1 _ H x _ _ H01). apply hinhfun. intros n. exists (pr1 n). abstract ( pattern (0%rig : X) at 1; rewrite <- (rigmultx0 X (nattorig (pr1 n))), nattorig_natmult ; exact (pr2 n)). Defined.
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.