proposition: Lemma isbinopfuntoabmonoidfrac (X : abmonoid) (A : submonoid X) : isbinopfun (toabmonoidfrac X A).
proof: Proof. unfold isbinopfun. intros x1 x2. change (paths (setquotpr _ (make_dirprod (x1 + x2) (@unel A))) (setquotpr (eqrelabmonoidfrac X A) (make_dirprod (x1 + x2) ((unel A) + (unel A))))). apply (maponpaths (setquotpr _)). apply (@pathsdirprod X A). apply idpath. apply (pathsinv0 (lunax A 0)). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders