Lemma isbinopfuntoabmonoidfrac (X : abmonoid) (A : submonoid X) : isbinopfun (toabmonoidfrac X A). Proof. unfold isbinopfun. intros x1 x2. change (setquotpr _ (x1 + x2 ,, @unel A) = setquotpr (eqrelabmonoidfrac X A) (x1 + x2 ,, unel A + unel A)). apply (maponpaths (setquotpr _)). apply (@pathsdirprod X A). apply idpath. exact (!lunax A 0). Defined.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.