Definition fldfrac (X : intdom) (is : isdeceq X) : fld. Proof. intros. exists (commringfrac X (intdomnonzerosubmonoid X)). split. - intro e. set (e' := zeroincommringfrac X (intdomnonzerosubmonoid X) (λ a : (intdomnonzerosubmonoid X), pr2 a) 1 (unel (intdomnonzerosubmonoid X)) e). apply (nonzeroax X e'). - intro x. induction (isdeceqfldfrac X is x 0) as [ e | ne ]. apply (ii2 e). apply ii1. exists (fldfracmultinv0 X is x). split. + apply (islinvinfldfrac X is x ne) . + apply (isrinvinfldfrac X is x ne). Defined.
Require Import UniMath.Algebra.Groups.