fact: Definition isincltofldfrac (X : intdom) (is : isdeceq X) : isincl (tofldfrac X is) := isincltocommringfrac X (intdomnonzerosubmonoid X) (λ x : _, pr2 (intdomiscancelable X (pr1 x) (pr2 x))).
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings