Definition hztohqandmult ( n m : hz ) : paths ( hztohq ( n * m )%hz ) ( hztohq n * hztohq m ) := isbinop2funtofldfrac hzintdom isdeceqhz n m .
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.