proposition: Lemma commringfracop1comp (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : iscomprelrelfun2 (eqrelcommringfrac X S) (eqrelcommringfrac X S) (commringfracop1int X S).
proof: Proof. intros. intros xs1 xs2 xs3 xs4. simpl. set (ff := @hinhfun2). simpl in ff. apply ff. clear ff. intros tt1 tt2. split with (@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). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids