Lemma isbinop1funtocommringfrac (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : @isbinopfun X (commringfrac X S) (tocommringfrac X S). Proof. intros. unfold isbinopfun. intros x x'. change (setquotpr (eqrelcommringfrac X S) (x + x' ,, unel S) = setquotpr _ (commringfracop1int X S (x ,, unel S) (x' ,, unel S))). apply (maponpaths (setquotpr _)). unfold commringfracop1int. simpl. apply pathsdirprod. - rewrite (ringlunax2 X _). rewrite (ringlunax2 X _). apply idpath. - change (unel S = op (unel S) (unel S)). exact (!runax S _). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.