Definition hztohqandminus ( n m : hz ) : paths ( hztohq ( n - m )%hz ) ( hztohq n - hztohq m ) := tofldfracandminus hzintdom isdeceqhz n m .
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.