Lemma isarchrig_isarchmonoid {X : rig} (R : hrel X) : R 1%rig 0%rig → istrans R → isbinophrel (X := rigaddabmonoid X) R → isarchrig R → isarchmonoid (X := rigaddabmonoid X) R. Proof. intros Hr1 Hr Hop1 H x y1 y2 Hy. split. - generalize (isarchrig_diff _ H _ _ Hy) (isarchrig_pos _ H x). apply hinhfun2. intros m n. exists (max 1 (pr1 n) * (pr1 m))%nat. apply isarchrig_isarchmonoid_1_aux. exact Hr1. exact Hr. exact Hop1. exact (pr2 m). exact (pr2 n). - generalize (isarchrig_diff _ H _ _ Hy) (isarchrig_gt _ H x). apply hinhfun2. intros m n. exists (max 1 (pr1 n) * (pr1 m))%nat. apply isarchrig_isarchmonoid_2_aux. exact Hr1. exact Hr. exact Hop1. exact (pr2 m). 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.