Definition hztohqandplus ( n m : hz ) : paths ( hztohq ( n + m )%hz ) ( hztohq n + hztohq m ) := isbinop1funtofldfrac hzintdom isdeceqhz n m .
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.