Definition isaddmonoidfuntofldfrac (X : intdom) (is : isdeceq X) : @ismonoidfun X (fldfrac X is) (tofldfrac X is) := isbinop1funtofldfrac X is ,, isunital1funtofldfrac X is.
Require Import UniMath.Algebra.Groups.