Definition intpartint0 ( xa : dirprod hz ( intdomnonzerosubmonoid hzintdom ) ) : nat := natdiv ( hzabsval (pr1 xa ) ) ( hzabsval ( pr1 ( pr2 xa ) ) ) .
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.