Definition weqfldfracgtint_b (X : intdom) {R : hrel X} (is1 : isringmultgt X R) (is2 : R 1 0) (ir : isirrefl R) (xa : X × ringpossubmonoid X is1 is2) : X × intdomnonzerosubmonoid X := pr1 xa ,, pr1 (pr2 xa) ,, rtoneq ir (pr2 (pr2 xa)).
Require Import UniMath.Algebra.Groups.