Definition tofldfracandminus (X : intdom) (is : isdeceq X) (x y : X) : tofldfrac X is (x - y) = tofldfrac X is x - tofldfrac X is y := tocommringfracandminus _ _ x y.
Require Import UniMath.Algebra.Groups.