Definition intpart0 : hq -> nat := setquotuniv ( eqrelabmonoidfrac hzmultabmonoid (intdomnonzerosubmonoid hzintdom) ) natset _ ( iscompintpartint0 ) .
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.