Definition hztohqandneq ( n m : hz ) ( is : hzneq n m ) : hqneq ( hztohq n ) ( hztohq m ) := negf ( invmaponpathsincl _ isinclhztohq n m ) is .
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.