Lemma isdeceqfldfrac (X : intdom) (is : isdeceq X) : isdeceq (commringfrac X (intdomnonzerosubmonoid X)). Proof. intros. apply isdeceqcommringfrac. - intro a. apply isrcancelableif. intros b0 b1 e. apply (intdomrcan X _ _ (pr1 a) (pr2 a) e). - apply is. Defined.
Require Import UniMath.Algebra.Groups.