fact: Definition tofldfracandminus (X : intdom) (is : isdeceq X) (x y : X) : paths (tofldfrac X is (x - y)) (tofldfrac X is x - tofldfrac X is y) := tocommringfracandminus _ _ x y.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings