proposition: Lemma isarchmonoid_isarchrig {X : rig} (R : hrel X) : (R 1%rig 0%rig) -> isarchmonoid (X := rigaddabmonoid X) R -> isarchrig R.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics