Lemma commringfracop1comp (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : iscomprelrelfun2 (eqrelcommringfrac X S) (eqrelcommringfrac X S) (commringfracop1int X S). Proof. intros. intros xs1 xs2 xs3 xs4. simpl. set (ff := @hinhfun2). simpl in ff. apply ff. clear ff. intros tt1 tt2. exists (@op S (pr1 tt1) (pr1 tt2)). set (eq1 := pr2 tt1). simpl in eq1. set (eq2 := pr2 tt2). simpl in eq2. unfold pr1carrier. apply (commringfracl1 X (pr1 xs1) (pr1 xs2) (pr1 xs3) (pr1 xs4) (pr1 (pr1 tt1)) (pr1 (pr1 tt2)) (pr1 (pr2 xs1)) (pr1 (pr2 xs2)) (pr1 (pr2 xs3)) (pr1 (pr2 xs4)) eq1 eq2). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.