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. intros. intros xa1 xa2. simpl. apply hinhfun. intro t2. exists (pr1 (pr1 t2) ,, rtoneq ir (pr2 (pr1 t2))). apply (pr2 t2). Defined.
Require Import UniMath.Algebra.Groups.