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