proposition: Lemma isbinop1funtocommringfrac (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : @isbinopfun X (commringfrac X S) (tocommringfrac X S).
proof: Proof. intros. unfold isbinopfun. intros x x'. change (paths (setquotpr _ (make_dirprod (x + x') (unel S))) (setquotpr (eqrelcommringfrac X S) (commringfracop1int X S (make_dirprod x (unel S)) (make_dirprod x' (unel S))))). apply (maponpaths (setquotpr _)). unfold commringfracop1int. simpl. apply pathsdirprod. - rewrite (ringlunax2 X _). rewrite (ringlunax2 X _). apply idpath. - change (paths (unel S) (op (unel S) (unel S))). apply (pathsinv0 (runax S _)). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids