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