Definition weqfldfracgt (X : intdom) (is : isdeceq X) {R : hrel X} (is0 : @isbinophrel X R) (is1 : isringmultgt X R) (is2 : R 1 0) (nc : neqchoice R) (ir : isirrefl R) : weq (fldfrac X is) (commringfrac X (ringpossubmonoid X is1 is2)). Proof. intros. set (f := weqfldfracgt_f X is is0 is1 is2 nc). set (g := weqfldfracgt_b X is is1 is2 ir). exists f. assert (egf : ∏ a, g (f a) = a). { unfold fldfrac. simpl. apply (setquotunivprop _ (λ a, make_hProp _ (isasetsetquot _ (g (f a)) a))). intro xa. simpl. change (setquotpr _ (weqfldfracgtint_b _ is1 is2 ir (weqfldfracgtint_f _ is0 _ _ nc xa)) = setquotpr (eqrelcommringfrac _ _) xa). apply (weqpathsinsetquot). simpl. apply hinhpr. exists ((1 : X) ,, nonzeroax X). simpl. unfold weqfldfracgtint_f. induction (nc (pr1 (pr2 xa)) 0 (pr2 (pr2 xa))) as [ g' | l' ]. - simpl. apply idpath. - simpl. rewrite (ringrmultminus X _ _). rewrite (ringlmultminus X _ _). apply idpath. } assert (efg : ∏ a, f (g a) = a). { unfold fldfrac. simpl. apply (setquotunivprop _ (λ a, make_hProp _ (isasetsetquot _ (f (g a)) a))). intro xa. simpl. change (setquotpr _ (weqfldfracgtint_f _ is0 is1 is2 nc (weqfldfracgtint_b _ _ _ ir xa)) = setquotpr (eqrelcommringfrac _ _) xa). apply weqpathsinsetquot. simpl. apply hinhpr. exists ((1 : X) ,, is2). unfold weqfldfracgtint_f. unfold weqfldfracgtint_b. simpl. set (int := nc (pr1 (pr2 xa)) 0 (rtoneq ir (pr2 (pr2 xa))) ). change (nc (pr1 (pr2 xa)) 0 (rtoneq ir (pr2 (pr2 xa)))) with int. induction int as [ g' | l' ]. - simpl. apply idpath. - simpl. rewrite (ringrmultminus X _ _). rewrite (ringlmultminus X _ _). apply idpath. } apply (isweq_iso _ _ egf efg). Defined.
Require Import UniMath.Algebra.Groups.