proposition: 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: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics