Lemma isringfunweqfldfracgt_f (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) : isringfun (weqfldfracgt_f X is is0 is1 is2 nc). Proof. intros. unfold weqfldfracgt_f. set (int := make_ringiso (invweq (weqfldfracgt X is is0 is1 is2 nc ir)) (isringfunweqfldfracgt_b X is is1 is2 ir)). change (@isringfun (fldfrac X is) (commringfrac X (ringpossubmonoid X is1 is2)) (invmap int)). apply isringfuninvmap. Qed.
Require Import UniMath.Algebra.Groups.