Lemma isbinop2funtofldfrac (X : intdom) (is : isdeceq X) : @isbinopfun (ringmultmonoid X) (ringmultmonoid (fldfrac X is)) (tofldfrac X is). Proof. apply (isbinopfuntoabmonoidfrac (ringmultabmonoid X)). Qed.
Require Import UniMath.Algebra.Groups.