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