fact: Definition isbinop2funtofldfrac (X : intdom) (is : isdeceq X) : @isbinopfun (ringmultmonoid X) (ringmultmonoid (fldfrac X is)) (tofldfrac X is) := isbinopfuntoabmonoidfrac (ringmultabmonoid X) (intdomnonzerosubmonoid X).
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings