proposition: Lemma weqfldfracgtintcomp_b (X : intdom) {R : hrel X} (is1 : isringmultgt X R) (is2 : R 1 0) (ir : isirrefl R) : iscomprelrelfun (eqrelcommringfrac X (ringpossubmonoid X is1 is2)) (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (weqfldfracgtint_b X is1 is2 ir).
proof: Proof. intros. intros xa1 xa2. simpl. apply hinhfun. intro t2. split with (tpair _ (pr1 (pr1 t2)) (rtoneq ir (pr2 (pr1 t2)))). apply (pr2 t2). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings