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