Lemma isarchabgrdiff {X : abmonoid} (R : hrel X) (Hr : isbinophrel R) : istrans R → isarchmonoid (setquot_aux R) → isarchgr (X := abgrdiff X) (abgrdiffrel X (L := R) Hr). Proof. intros Hr' H. simple refine (setquotuniv3prop _ (λ x y1 y2, (abgrdiffrel X Hr y1 y2 → ∃ n : nat, abgrdiffrel X Hr (natmult (X := abgrdiff X) n y1 * x)%multmonoid (natmult (X := abgrdiff X) n y2)) ,, _) _). abstract apply isapropimpl, propproperty. intros x y1 y2 Hy. eapply hinhfun2. 2: apply (isarchmonoid_1 _ H (pr1 x) (pr1 y1 * pr2 y2)%multmonoid (pr1 y2 * pr2 y1)%multmonoid), Hy. 2: apply (isarchmonoid_2 _ H (pr2 x) (pr1 y1 * pr2 y2)%multmonoid (pr1 y2 * pr2 y1)%multmonoid), Hy. intros n1 n2. exists (pr1 n1 + pr1 n2)%nat. apply isarchabgrdiff_aux. exact Hr'. exact (pr2 n1). exact (pr2 n2). 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.